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.TFAE: For a Bézout domain, noetherian ↔ PID ↔ UFD ↔ ACCP

theorem IsBezout.iff_span_pair_isPrincipal {R : Type u} [CommRing R] : IsBezout R ↔ ∀ (x y : R), Submodule.IsPrincipal (Ideal.span {x, y})

theorem Function.Surjective.isBezout {R : Type u} [CommRing R] {S : Type v} [CommRing S] (f : R →+* S) (hf : Function.Surjective ⇑f) [IsBezout R] : IsBezout S

theorem IsBezout.TFAE {R : Type u} [CommRing R] [IsBezout R] [IsDomain R] : List.TFAE [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R]