# mathlib3documentation

ring_theory.bezout

# Bézout rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Main results #

• is_bezout.iff_span_pair_is_principal: It suffices to verify every span {x, y} is principal.
• is_bezout.to_gcd_monoid: Every Bézout domain is a GCD domain. This is not an instance.
• is_bezout.tfae: For a Bézout domain, noetherian ↔ PID ↔ UFD ↔ ACCP
@[class]
structure is_bezout (R : Type u) [comm_ring R] :
Prop
• is_principal_of_fg : (I : ideal R),

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

Instances of this typeclass
@[protected, instance]
noncomputable def is_bezout.gcd {R : Type u} [comm_ring R] [is_bezout R] (x y : R) :
R

The gcd of two elements in a bezout domain.

Equations
theorem is_bezout.span_gcd {R : Type u} [comm_ring R] [is_bezout R] (x y : R) :
theorem is_bezout.gcd_dvd_left {R : Type u} [comm_ring R] [is_bezout R] (x y : R) :
x
theorem is_bezout.gcd_dvd_right {R : Type u} [comm_ring R] [is_bezout R] (x y : R) :
y
theorem is_bezout.dvd_gcd {R : Type u} [comm_ring R] [is_bezout R] {x y z : R} (hx : z x) (hy : z y) :
z
theorem is_bezout.gcd_eq_sum {R : Type u} [comm_ring R] [is_bezout R] (x y : R) :
(a b : R), a * x + b * y =
noncomputable def is_bezout.to_gcd_domain (R : Type u) [comm_ring R] [is_bezout R] [is_domain R] [decidable_eq R] :

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

Equations
@[protected, instance]
theorem function.surjective.is_bezout {R : Type u} [comm_ring R] {S : Type v} [comm_ring S] (f : R →+* S) (hf : function.surjective f) [is_bezout R] :
@[protected, instance]
theorem is_bezout.tfae {R : Type u} [comm_ring R] [is_bezout R] [is_domain R] :