dvd_antisymm'

Mathlib.Algebra.GroupWithZero.Divisibility

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

English

If a|b and b|a in a CancelCommMonoidWithZero with Units ⊣, then b = a.

Русский

Если a|b и b|a в CancelCommMonoidWithZero с условием на единицы, то b = a.

LaTeX

$$a \mid b \land b \mid a \Rightarrow b = a$$

Lean4

theorem dvd_antisymm' : a ∣ b → b ∣ a → b = a :=
  flip dvd_antisymm

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

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

Разделы

Аффилиация

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