dvd_antisymm

Mathlib.SetTheory.Ordinal.Arithmetic

URI: https://scilib.ai/kg/mathlib#Ordinal.dvd_antisymm

← MathLib Explorer

English

If a ∣ b and b ∣ a, then a = b.

Русский

Если a делит b и b делит a, то a = b.

LaTeX

$$∀ {a b : \\operatorname{Ordinal}}, a ∣ b → b ∣ a → a = b$$

Lean4

theorem dvd_antisymm {a b : Ordinal} (h₁ : a ∣ b) (h₂ : b ∣ a) : a = b :=
  if a0 : a = 0 then by subst a; exact (eq_zero_of_zero_dvd h₁).symm
  else if b0 : b = 0 then by subst b; exact eq_zero_of_zero_dvd h₂ else (le_of_dvd b0 h₁).antisymm (le_of_dvd a0 h₂)

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

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

Разделы

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

Аффилиация

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