subsingleton_gcdMonoid_of_unique_units

English

In a gcd-monoid α, lcm(m,n) divides m·n.

Русский

В gcd-монойде α lcm(m,n) делит m·n.

LaTeX

$$$$ \\forall m,n:\\, \\operatorname{lcm}(m,n) \\mid m n. $$$$

Lean4

instance subsingleton_gcdMonoid_of_unique_units : Subsingleton (GCDMonoid α) :=
  ⟨fun g₁ g₂ =>
    by
    have hgcd : g₁.gcd = g₂.gcd := by
      ext a b
      refine associated_iff_eq.mp (associated_of_dvd_dvd ?_ ?_) <;>
        apply_rules +allowSynthFailures [dvd_gcd, gcd_dvd_left, gcd_dvd_right]
    have hlcm : g₁.lcm = g₂.lcm := by
      ext a b
      refine associated_iff_eq.mp (associated_of_dvd_dvd ?_ ?_) <;>
        apply_rules +allowSynthFailures [lcm_dvd, dvd_lcm_left, dvd_lcm_right]
    cases g₁
    cases g₂
    dsimp only at hgcd hlcm
    simp only [hgcd, hlcm]⟩

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