dvd_of_mk_le_mk

Mathlib.Algebra.GroupWithZero.Associated

URI: https://scilib.ai/kg/mathlib#Associates.dvd_of_mk_le_mk

English

If mk(a) ≤ mk(b) then a divides b.

Русский

Если mk(a) ≤ mk(b), то a делится на b.

LaTeX

$$$ \operatorname{mk} a \le \operatorname{mk} b \Rightarrow a \mid b $$$

Lean4

theorem dvd_of_mk_le_mk {a b : M} : Associates.mk a ≤ Associates.mk b → a ∣ b :=
  mk_dvd_mk.mp

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

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

Разделы

Аффилиация

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