Principal ideal rings and principal ideal domains #
A principal ideal ring (PIR) is a ring in which all left ideals are principal. A principal ideal domain (PID) is an integral domain which is a principal ideal ring.
Main definitions #
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 rings, saying that every left 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
Main results #
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 ring is a principal ideal ring if all (left) 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