English
If d divides a and b and every e dividing a,b also divides d, then gcd(a,b) is associated to d.
Русский
Если d делит A и B, и каждое e, делящее A и B, делит d, тогда gcd(a,b) ассоциирован с d.
LaTeX
$$$(d \\mid a) \\land (d \\mid b) \\land (\\\\forall e, e \\mid a \\rightarrow e \\mid b \\\\rightarrow e \\mid d) \\\\Rightarrow gcd(a,b) = normalize(d)$$$
Lean4
theorem gcd_greatest {α : Type*} [CancelCommMonoidWithZero α] [NormalizedGCDMonoid α] {a b d : α} (hda : d ∣ a)
(hdb : d ∣ b) (hd : ∀ e : α, e ∣ a → e ∣ b → e ∣ d) : GCDMonoid.gcd a b = normalize d :=
haveI h := hd _ (GCDMonoid.gcd_dvd_left a b) (GCDMonoid.gcd_dvd_right a b)
gcd_eq_normalize h (GCDMonoid.dvd_gcd hda hdb)
