dvd_eq_le — Mathlib

English

Divisibility on Associates M coincides with the induced order: a | b iff a ≤ b.

Русский

Делимость на Associates(M) совпадает с соответствующим порядком: a делится на b, если и только если a ≤ b.

LaTeX

$$$ \forall a,b : \operatorname{Associates}(M), \operatorname{Dvd}.dvd(a,b) \iff a \le b $$$

Lean4

theorem dvd_eq_le : ((· ∣ ·) : Associates M → Associates M → Prop) = (· ≤ ·) :=
  rfl

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