English
In a NormalizedGCDMonoid, lcm is associative: lcm(lcm(m,n),k) = lcm(m, lcm(n,k)).
Русский
В нормализованном gcd-монойде НОК ассоциативна: lcm(lcm(m,n),k) = lcm(m, lcm(n,k)).
LaTeX
$$$ \operatorname{lcm}(\operatorname{lcm}(m,n),k) = \operatorname{lcm}(m, \operatorname{lcm}(n,k)) $$$
Lean4
theorem lcm_assoc [NormalizedGCDMonoid α] (m n k : α) : lcm (lcm m n) k = lcm m (lcm n k) :=
dvd_antisymm_of_normalize_eq (normalize_lcm _ _) (normalize_lcm _ _)
(lcm_dvd (lcm_dvd (dvd_lcm_left _ _) ((dvd_lcm_left _ _).trans (dvd_lcm_right _ _)))
((dvd_lcm_right _ _).trans (dvd_lcm_right _ _)))
(lcm_dvd ((dvd_lcm_left _ _).trans (dvd_lcm_left _ _))
(lcm_dvd ((dvd_lcm_right _ _).trans (dvd_lcm_left _ _)) (dvd_lcm_right _ _)))
