English
Let α be a type equipped with a CancelCommMonoidWithZero structure and a NormalizedGCDMonoid structure. For all a,b,c ∈ α, if gcd(a,b) divides c and c divides gcd(a,b), then gcd(a,b) equals normalize(c).
Русский
Пусть α имеет структуруCancelCommMonoidWithZero и нормализованный НОД-монад. Для любых a,b,c ∈ α выполняется: gcd(a,b) | c и c | gcd(a,b) тогда gcd(a,b) = normalize(c).
LaTeX
$$$$ \forall a,b,c \in \alpha\;\big( \gcd(a,b) \mid c \land c \mid \gcd(a,b) \big) \Rightarrow \gcd(a,b) = \operatorname{normalize}(c) $$$$
Lean4
theorem gcd_eq_normalize [NormalizedGCDMonoid α] {a b c : α} (habc : gcd a b ∣ c) (hcab : c ∣ gcd a b) :
gcd a b = normalize c :=
normalize_gcd a b ▸ normalize_eq_normalize habc hcab
