English
If d divides a and b and every e dividing a,b also divides d, then gcd(a,b) is associated to d (right variant).
Русский
Если 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 Associated (gcd a b) d$$$
Lean4
theorem gcd_greatest_associated {α : Type*} [CancelCommMonoidWithZero α] [GCDMonoid α] {a b d : α} (hda : d ∣ a)
(hdb : d ∣ b) (hd : ∀ e : α, e ∣ a → e ∣ b → e ∣ d) : Associated d (GCDMonoid.gcd a b) :=
haveI h := hd _ (GCDMonoid.gcd_dvd_left a b) (GCDMonoid.gcd_dvd_right a b)
associated_of_dvd_dvd (GCDMonoid.dvd_gcd hda hdb) h
