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 everyspan {x, y}
is principal.IsBezout.TFAE
: For a Bézout domain, noetherian ↔ PID ↔ UFD ↔ ACCP