dvd_out_iff — Mathlib

English

Let α be a CancelCommMonoidWithZero and α be NormalizationMonoid. For a ∈ α and b ∈ Associates α, a divides b.out if and only if the associate class of a is below b, i.e. mk a ≤ b.

Русский

Пусть α имеет CancelCommMonoidWithZero и NormalizationMonoid. Для a ∈ α и b ∈ Associates α, a делит b.out тогда и только тогда, когда класс ассоциированного a лежит ниже b, то есть mk a ≤ b.

LaTeX

$$$$ a \\mid b.out \\iff \\operatorname{mk} a \\le b $$$$

Lean4

theorem dvd_out_iff (a : α) (b : Associates α) : a ∣ b.out ↔ Associates.mk a ≤ b :=
  Quotient.inductionOn b <| by simp [Associates.out_mk, Associates.quotient_mk_eq_mk, mk_le_mk_iff_dvd]

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