instPreorder

Mathlib.Algebra.GroupWithZero.Associated

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

English

The relation on Associates M given by divisibility defines a preorder: a ≤ b iff a divides b.

Русский

Отношение по делимости на Associates(M) задаёт предобозрение: a ≤ b тогда и только если a делится на b.

LaTeX

$$$ a \le b \iff \operatorname{Dvd}.dvd(a,b) $$$

Lean4

instance instPreorder : Preorder (Associates M) where
  le := Dvd.dvd
  le_refl := dvd_refl
  le_trans _ _ _ := dvd_trans

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

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

Разделы

Аффилиация

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