mk_le_mk_of_dvd — Mathlib

English

Let M be a commutative monoid. If a divides b, then the associate class of a is below the associate class of b in the natural divisibility order on the set of associates of M.

Русский

Пусть M — коммутативный моноид. Если a делится на b (a | b), то класс ассоциированности a находится ниже класса ассоциированности b в естественном порядке делимости на множестве ассоциированных элементов M.

LaTeX

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

Lean4

theorem mk_le_mk_of_dvd {a b : M} : a ∣ b → Associates.mk a ≤ Associates.mk b :=
  mk_dvd_mk.mpr

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