lcm_eq_of_associated_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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