mk_le_mk_iff_dvd

Mathlib.Algebra.GroupWithZero.Associated

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

English

Let a,b be elements of M. The associate classes satisfy [a] ≤ [b] if and only if a ∣ b.

Русский

Пусть a,b принадлежат M. Классы ассоциированности удовлетворяют [a] ≤ [b], если и только если a делится на b.

LaTeX

$$$ [a] \le [b] \iff a \mid b $$$

Lean4

theorem mk_le_mk_iff_dvd {a b : M} : Associates.mk a ≤ Associates.mk b ↔ a ∣ b :=
  mk_dvd_mk

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

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

Разделы

Аффилиация

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