English
In a Euclidean domain with finite gcd monoid, the ideal generated by gcd(x,y) equals the ideal generated by {x,y}. This is the Bézout property expressed in the span of the gcd.
Русский
В евклидовом домене, где gcd-монод конечен, идеал, порождаемый gcd(x,y), совпадает с идеалом, порождаемым множеством {x,y}. Это свойство Безу в форме спана gcd.
LaTeX
$$$\\operatorname{span}\\{\\gcd(x,y)\\} = \\operatorname{span}\\{x,y\\}$$$
Lean4
/-- Create a `GCDMonoid` whose `GCDMonoid.gcd` matches `EuclideanDomain.gcd`. -/
def gcdMonoid (R) [EuclideanDomain R] [DecidableEq R] : GCDMonoid R
where
gcd := gcd
lcm := lcm
gcd_dvd_left := gcd_dvd_left
gcd_dvd_right := gcd_dvd_right
dvd_gcd := dvd_gcd
gcd_mul_lcm a b := by rw [EuclideanDomain.gcd_mul_lcm]
lcm_zero_left := lcm_zero_left
lcm_zero_right := lcm_zero_right
