lcm_comm' — Mathlib

English

For normalized gcd monoids, lcm(a,b) and lcm(b,a) are associated; more precisely, lcm(a,b) ∼ lcm(b,a).

Русский

Для нормализованных gcd-монойдов НОК(a,b) ассоциирована с НОК(b,a).

LaTeX

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

Lean4

theorem lcm_comm' [GCDMonoid α] (a b : α) : Associated (lcm a b) (lcm b a) :=
  associated_of_dvd_dvd (lcm_dvd (dvd_lcm_right _ _) (dvd_lcm_left _ _))
    (lcm_dvd (dvd_lcm_right _ _) (dvd_lcm_left _ _))

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