English
For a, b, c in a normalized gcd monoid α, gcd(a·b, a·c) = normalize(a) · gcd(b,c).
Русский
Для любых a,b,c в нормализованном НОД-моноде α: gcd(a·b, a·c) = normalize(a) · gcd(b,c).
LaTeX
$$$$ \gcd(a \cdot b, a \cdot c) = \operatorname{normalize}(a) \cdot \gcd(b,c) $$$$
Lean4
@[simp]
theorem gcd_mul_left [NormalizedGCDMonoid α] (a b c : α) : gcd (a * b) (a * c) = normalize a * gcd b c :=
(by_cases (by rintro rfl; simp only [zero_mul, gcd_zero_left, normalize_zero])) fun ha : a ≠ 0 =>
suffices gcd (a * b) (a * c) = normalize (a * gcd b c) by simpa
let ⟨d, eq⟩ := dvd_gcd (dvd_mul_right a b) (dvd_mul_right a c)
gcd_eq_normalize
(eq.symm ▸
mul_dvd_mul_left a
(show d ∣ gcd b c from
dvd_gcd ((mul_dvd_mul_iff_left ha).1 <| eq ▸ gcd_dvd_left _ _)
((mul_dvd_mul_iff_left ha).1 <| eq ▸ gcd_dvd_right _ _)))
(dvd_gcd (mul_dvd_mul_left a <| gcd_dvd_left _ _) (mul_dvd_mul_left a <| gcd_dvd_right _ _))
