lcm_comm — Mathlib

English

In a NormalizedGCDMonoid, lcm(a,b) = lcm(b,a).

Русский

В нормализованном gcd-монойде НОК симметрична: lcm(a,b) = lcm(b,a).

LaTeX

$$$ \operatorname{lcm}(a,b) = \operatorname{lcm}(b,a) $$$

Lean4

theorem lcm_comm [NormalizedGCDMonoid α] (a b : α) : lcm a b = lcm b a :=
  dvd_antisymm_of_normalize_eq (normalize_lcm _ _) (normalize_lcm _ _) (lcm_dvd (dvd_lcm_right _ _) (dvd_lcm_left _ _))
    (lcm_dvd (dvd_lcm_right _ _) (dvd_lcm_left _ _))

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