mathlib3 documentation

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 #

@[class]
structure is_bezout (R : Type u) [comm_ring R] :
Prop

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) :
theorem is_bezout.gcd_dvd_right {R : Type u} [comm_ring R] [is_bezout R] (x y : R) :
theorem is_bezout.dvd_gcd {R : Type u} [comm_ring R] [is_bezout R] {x y z : R} (hx : z x) (hy : z y) :
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 = is_bezout.gcd x 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] :