eq_of_associated_of_nonneg

Mathlib.Algebra.GCDMonoid.Nat

URI: https://scilib.ai/kg/mathlib#Int.eq_of_associated_of_nonneg

← MathLib Explorer

English

If a is associated to b and a,b ≥ 0, then a = b.

Русский

Если a ассоциировано с b и a,b ≥ 0, то a = b.

LaTeX

$$(\operatorname{Associated}(a,b) \land a \ge 0 \land b \ge 0) \Rightarrow a = b$$

Lean4

theorem eq_of_associated_of_nonneg {a b : ℤ} (h : Associated a b) (ha : 0 ≤ a) (hb : 0 ≤ b) : a = b :=
  dvd_antisymm_of_normalize_eq (normalize_of_nonneg ha) (normalize_of_nonneg hb) h.dvd h.symm.dvd

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru