English
For any a,b in M, mk(a) divides mk(b) iff a divides b.
Русский
Для любых a,b ∈ Mdk mk(a) делится на mk(b) тогда и только тогда, когда a делится на b.
LaTeX
$$$ \forall {a,b : M}, \operatorname{Associates.mk} a \mid \operatorname{Associates.mk} b \iff a \mid b $$$
Lean4
@[simp]
theorem mk_dvd_mk {a b : M} : Associates.mk a ∣ Associates.mk b ↔ a ∣ b :=
by
simp only [dvd_def, mk_surjective.exists, mk_mul_mk, mk_eq_mk_iff_associated, Associated.comm (x := b)]
constructor
· rintro ⟨x, u, rfl⟩
exact ⟨_, mul_assoc ..⟩
· rintro ⟨c, rfl⟩
use c