dvd_antisymm

Mathlib.Data.PNat.Basic

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

English

If m ∣ n and n ∣ m then m = n.

Русский

Если m делит n и n делит m, то m = n.

LaTeX

$$$$ (m \mid n) \wedge (n \mid m) \Rightarrow m = n $$$$

Lean4

theorem dvd_antisymm {m n : ℕ+} : m ∣ n → n ∣ m → m = n := fun hmn hnm => (le_of_dvd hmn).antisymm (le_of_dvd hnm)

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

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

Разделы

Аффилиация

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