English
For a,b,c in α, gcd((a·b), (a·c)) is associated with a·gcd(b,c).
Русский
Для любой тройки a,b,c: gcd(a·b, a·c) ассоциировано с a·gcd(b,c).
LaTeX
$$$$ \text{Associated}(\gcd(a\cdot b, a\cdot c), a\cdot \gcd(b,c)) $$$$
Lean4
theorem gcd_mul_left' [GCDMonoid α] (a b c : α) : Associated (gcd (a * b) (a * c)) (a * gcd b c) :=
by
obtain rfl | ha := eq_or_ne a 0
· simp only [zero_mul, gcd_zero_left']
obtain ⟨d, eq⟩ := dvd_gcd (dvd_mul_right a b) (dvd_mul_right a c)
apply associated_of_dvd_dvd
· rw [eq]
gcongr
exact
dvd_gcd ((mul_dvd_mul_iff_left ha).1 <| eq ▸ gcd_dvd_left _ _)
((mul_dvd_mul_iff_left ha).1 <| eq ▸ gcd_dvd_right _ _)
· exact dvd_gcd (mul_dvd_mul_left a <| gcd_dvd_left _ _) (mul_dvd_mul_left a <| gcd_dvd_right _ _)
