mk_dvd_mk — Mathlib

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

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