dvd_antisymm_of_normalize_eq

Mathlib.Algebra.GCDMonoid.Basic

URI: https://scilib.ai/kg/mathlib#dvd_antisymm_of_normalize_eq

← MathLib Explorer

English

If ha, hb, hab, hba hold, then a = b

Русский

Если выполнены ha, hb, hab, hba, то a = b

LaTeX

$$$ a \text{ normalized } \Rightarrow a = b \Rightarrow b \text{ normalized } \Rightarrow a = b. $$$

Lean4

theorem dvd_antisymm_of_normalize_eq {a b : α} (ha : normalize a = a) (hb : normalize b = b) (hab : a ∣ b)
    (hba : b ∣ a) : a = b :=
  ha ▸ hb ▸ normalize_eq_normalize hab hba

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

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

Разделы

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

Аффилиация

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