gcd_isUnit_iff — Mathlib

English

In a Bézout ring, gcd(x,y) is a unit if and only if x and y are coprime.

Русский

В кольце Безоу gcd(x,y) является единицей тогда и только тогда, когда x и y взаимно просты.

LaTeX

$$$\forall x,y \in R,\; \mathrm{IsUnit}(\gcd(x,y)) \iff \mathrm{IsCoprime}(x,y)$$$

Lean4

theorem gcd_isUnit_iff (x y : R) : IsUnit (gcd x y) ↔ IsCoprime x y := by
  rw [IsCoprime, ← Ideal.mem_span_pair, ← span_gcd, ← span_singleton_eq_top, eq_top_iff_one]

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