gcd_comm — Mathlib

English

In a NormalizedGCDMonoid α, gcd is commutative: gcd(a,b) = gcd(b,a).

Русский

В нормализованном gcd-монойде α функция gcd симметрична: gcd(a,b) = gcd(b,a).

LaTeX

$$$$ \\gcd(a,b) = \\gcd(b,a) $$$$

Lean4

theorem gcd_comm [NormalizedGCDMonoid α] (a b : α) : gcd a b = gcd b a :=
  dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _) (dvd_gcd (gcd_dvd_right _ _) (gcd_dvd_left _ _))
    (dvd_gcd (gcd_dvd_right _ _) (gcd_dvd_left _ _))

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