# Documentation

Mathlib.RingTheory.Bezout

# Bézout rings #

A Bézout ring (Bezout ring) is a ring whose finitely generated ideals are principal. Notable examples include principal ideal rings, valuation rings, and the ring of algebraic integers.

## Main results #

• IsBezout.iff_span_pair_isPrincipal: It suffices to verify every span {x, y} is principal.
• IsBezout.toGCDDomain: Every Bézout domain is a GCD domain. This is not an instance.
• IsBezout.TFAE: For a Bézout domain, noetherian ↔ PID ↔ UFD ↔ ACCP
class IsBezout (R : Type u) [] :
• isPrincipal_of_FG : ∀ (I : ),

Any finitely generated ideal is principal.

A Bézout ring is a ring whose finitely generated ideals are principal.

Instances
instance IsBezout.span_pair_isPrincipal {R : Type u} [] [] (x : R) (y : R) :
noncomputable def IsBezout.gcd {R : Type u} [] [] (x : R) (y : R) :
R

The gcd of two elements in a bezout domain.

Instances For
theorem IsBezout.span_gcd {R : Type u} [] [] (x : R) (y : R) :
theorem IsBezout.gcd_dvd_left {R : Type u} [] [] (x : R) (y : R) :
x
theorem IsBezout.gcd_dvd_right {R : Type u} [] [] (x : R) (y : R) :
y
theorem IsBezout.dvd_gcd {R : Type u} [] [] {x : R} {y : R} {z : R} (hx : z x) (hy : z y) :
z
theorem IsBezout.gcd_eq_sum {R : Type u} [] [] (x : R) (y : R) :
a b, a * x + b * y =
noncomputable def IsBezout.toGCDDomain (R : Type u) [] [] [] [] :

Any bezout domain is a GCD domain. This is not an instance since GCDMonoid contains data, and this might not be how we would like to construct it.

Instances For
instance IsBezout.instIsIntegrallyClosed {R : Type u} [] [] [] :
theorem Function.Surjective.isBezout {R : Type u} [] {S : Type v} [] (f : R →+* S) (hf : ) [] :
theorem IsBezout.TFAE {R : Type u} [] [] [] :