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.
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 principal_ideal_ring namespace.
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_domain: a noncomputable definition, putting a UFD structure on a PID. Note that the definition of a UFD is currently not a predicate, as it contains data of factorizations of non-zero elements.
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.
- principal : ∀ (S : ideal R), submodule.is_principal S
A commutative ring is a principal ideal ring if all ideals are principal.
generator I, if I is a principal submodule, is the x ∈ M such that span R {x} = I
Equations
Equations
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 _)
The unique factorization domain structure given by the principal ideal domain.
This is not added as type class instance, since the factors might be computed in a different way.
E.g. factors could return normalized values.
Equations
- principal_ideal_ring.to_unique_factorization_domain = {factors := principal_ideal_ring.factors _inst_2, factors_prod := _, prime_factors := _}