span_gcd — Mathlib

English

In a Euclidean domain, gcd(x,y) is a unit if and only if x and y are coprime. This is the standard characterization linking gcd units and coprimality.

Русский

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

LaTeX

$$$\\gcd(x,y) \\in \\mathcal{U} \\iff \\text{IsCoprime}(x,y).$$$

Lean4

theorem span_gcd [DecidableEq α] (x y : α) : span ({gcd x y} : Set α) = span ({ x, y } : Set α) :=
  letI := EuclideanDomain.gcdMonoid α
  _root_.span_gcd x y

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