English
Let α be CancelCommMonoidWithZero and NormalizationMonoid α. For a ∈ α and b ∈ Associates α, b.out divides a if and only if b ≤ mk a.
Русский
Пусть α имеет CancelCommMonoidWithZero и NormalizationMonoid. Для a ∈ α и b ∈ Associates α, b.out делит a тогда и только тогда, когда b ≤ mk a.
LaTeX
$$$$ b.out \\mid a \\iff b \\le \\operatorname{mk} a $$$$
Lean4
theorem out_dvd_iff (a : α) (b : Associates α) : b.out ∣ a ↔ b ≤ Associates.mk a :=
Quotient.inductionOn b <| by simp [Associates.out_mk, Associates.quotient_mk_eq_mk, mk_le_mk_iff_dvd]