English
In a NormalizedGCDMonoid α, lcm((a·b),(a·c)) = normalize(a) · lcm(b,c), with a ≠ 0, and a special case for a = 0.
Русский
В нормализованном gcd-монойде lcm(a·b, a·c) = normalize(a) · lcm(b,c); при a = 0 отдельно.
LaTeX
$$$ \operatorname{lcm}(a\cdot b, a\cdot c) = \operatorname{normalize}(a) \cdot \operatorname{lcm}(b,c) $$$
Lean4
@[simp]
theorem lcm_mul_left [NormalizedGCDMonoid α] (a b c : α) : lcm (a * b) (a * c) = normalize a * lcm b c :=
(by_cases (by rintro rfl; simp only [zero_mul, lcm_zero_left, normalize_zero])) fun ha : a ≠ 0 =>
suffices lcm (a * b) (a * c) = normalize (a * lcm b c) by simpa
have : a ∣ lcm (a * b) (a * c) := (dvd_mul_right _ _).trans (dvd_lcm_left _ _)
let ⟨_, eq⟩ := this
lcm_eq_normalize (lcm_dvd (mul_dvd_mul_left a (dvd_lcm_left _ _)) (mul_dvd_mul_left a (dvd_lcm_right _ _)))
(eq.symm ▸
(mul_dvd_mul_left a <|
lcm_dvd ((mul_dvd_mul_iff_left ha).1 <| eq ▸ dvd_lcm_left _ _)
((mul_dvd_mul_iff_left ha).1 <| eq ▸ dvd_lcm_right _ _)))
