Principal ideal rings and principal ideal domains
A principal ideal ring (PIR) is a commutative ring in which all ideals are principal. A principal ideal domain (PID) is an integral domain which is a principal ideal ring.
Note that for principal ideal domains, one should use
[integral domain R] [is_principal_ideal_ring R]. There is no explicit definition of a PID.
Theorems about PID's are in the
is_principal_ideal_ring: a predicate on commutative rings, saying that every ideal is principal.
generator: a generator of a principal ideal (or more generally submodule)
to_unique_factorization_monoid: a PID is a unique factorization domain
to_maximal_ideal: a non-zero prime ideal in a PID is maximal.
euclidean_domain.to_principal_ideal_domain: a Euclidean domain is a PID.
M is principal if it is generated by one element.
A commutative ring is a principal ideal ring if all ideals are principal.
factors a is a multiset of irreducible elements whose product is
a, up to units
ring_hom maps all units and all factors of an element
a into a submonoid
s, then it
a into that submonoid.
A principal ideal domain has unique factorization