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]