English
In a gcd-monoid α, for all a,b,c in α, a divides gcd(b,c) iff a divides b and a divides c.
Русский
В gcd-монойде α для любых a,b,c верно: a делит gcd(b,c) тогда и только тогда, когда a делит b и a делит c.
LaTeX
$$$$ a \\mid \\gcd(b,c) \\iff (a \\mid b \\land a \\mid c) $$$$
Lean4
theorem dvd_gcd_iff [GCDMonoid α] (a b c : α) : a ∣ gcd b c ↔ a ∣ b ∧ a ∣ c :=
Iff.intro (fun h => ⟨h.trans (gcd_dvd_left _ _), h.trans (gcd_dvd_right _ _)⟩) fun ⟨hab, hac⟩ => dvd_gcd hab hac