English
For any k,m,n, gcd(k, m) · gcd(k, n) is a multiple of gcd(k, m n).
Русский
Для любых k,m,n произведение gcd(k,m) и gcd(k,n) является делителем gcd(k, m n).
LaTeX
$$$\\\\gcd k m \\\\cdot \\\\gcd k n \\\\mid \\\\gcd k (m n)$$$
Lean4
theorem gcd_mul_dvd_mul_gcd [GCDMonoid α] (k m n : α) : gcd k (m * n) ∣ gcd k m * gcd k n :=
by
obtain ⟨m', n', hm', hn', h⟩ := exists_dvd_and_dvd_of_dvd_mul (gcd_dvd_right k (m * n))
replace h : gcd k (m * n) = m' * n' := h
rw [h]
have hm'n' : m' * n' ∣ k := h ▸ gcd_dvd_left _ _
apply mul_dvd_mul
· have hm'k : m' ∣ k := (dvd_mul_right m' n').trans hm'n'
exact dvd_gcd hm'k hm'
· have hn'k : n' ∣ k := (dvd_mul_left n' m').trans hm'n'
exact dvd_gcd hn'k hn'
