gcd_isUnit_iff_isRelPrime — Mathlib

English

For any a,b in a gcd-monoid α, gcd(a,b) is a unit iff a and b are relatively prime.

Русский

Для любых a,b в gcd-монойде α, gcd(a,b) является единицей тогда и только тогда, когда a и b взаимно просты.

LaTeX

$$$$ \\IsUnit(\\gcd(a,b)) \\iff \\IsRelPrime(a,b) $$$$

Lean4

theorem gcd_isUnit_iff_isRelPrime [GCDMonoid α] {a b : α} : IsUnit (gcd a b) ↔ IsRelPrime a b :=
  ⟨fun h _ ha hb ↦ isUnit_of_dvd_unit (dvd_gcd ha hb) h, (· (gcd_dvd_left a b) (gcd_dvd_right a b))⟩

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