dvd_gcd_iff — Mathlib

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

Похожие утверждения