lcm_eq_of_associated_left — Mathlib

English

If m and n are associated in a normalized gcd-monoid, then for every k, lcm(m,k) = lcm(n,k).

Русский

Если m и n ассоциированы в нормализованном gcd-монойде, то для каждого k выполняется lcm(m,k) = lcm(n,k).

LaTeX

$$$$ \\forall k:\\, lcm(m,k) = lcm(n,k) \\quad \\text{whenever } \\mathrm{Associated}(m,n) $$$$

Lean4

theorem lcm_eq_of_associated_left [NormalizedGCDMonoid α] {m n : α} (h : Associated m n) (k : α) : lcm m k = lcm n k :=
  dvd_antisymm_of_normalize_eq (normalize_lcm _ _) (normalize_lcm _ _) (lcm_dvd_lcm h.dvd dvd_rfl)
    (lcm_dvd_lcm h.symm.dvd dvd_rfl)

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