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
[is_domain R] [is_principal_ideal_ring R]
. There is no explicit definition of a PID.
Theorems about PID's are in the principal_ideal_ring
namespace.
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.
- principal : ∃ (a : M), S = submodule.span R {a}
An R
-submodule of M
is principal if it is generated by one element.
Instances of this typeclass
- principal : ∀ (S : ideal R), submodule.is_principal S
A ring is a principal ideal ring if all (left) ideals are principal.
generator I
, if I
is a principal submodule, is an x ∈ M
such that span R {x} = I
Equations
factors a
is a multiset of irreducible elements whose product is a
, up to units
Equations
- principal_ideal_ring.factors a = dite (a = 0) (λ (h : a = 0), ∅) (λ (h : ¬a = 0), classical.some _)
If a ring_hom
maps all units and all factors of an element a
into a submonoid s
, then it
also maps a
into that submonoid.
A principal ideal domain has unique factorization
The surjective image of a principal ideal ring is again a principal ideal ring.
Bézout's lemma