mathlib documentation


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.

Main results

structure submodule.is_principal {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] (S : submodule R M) :

An R-submodule of M is principal if it is generated by one element.

structure is_principal_ideal_ring (R : Type u) [comm_ring R] :

A commutative ring is a principal ideal ring if all ideals are principal.

def submodule.is_principal.generator {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (S : submodule R M) [S.is_principal] :

generator I, if I is a principal submodule, is an x ∈ M such that span R {x} = I


theorem submodule.is_principal.mem_iff_eq_smul_generator {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M] (S : submodule R M) [S.is_principal] {x : M} :

theorem is_prime.to_maximal_ideal {R : Type u} [integral_domain R] [is_principal_ideal_ring R] {S : ideal R} [hpi : S.is_prime] (hS : S ) :

theorem mod_mem_iff {R : Type u} [euclidean_domain R] {S : ideal R} {x y : R} (hy : y S) :
x % y S x S

factors a is a multiset of irreducible elements whose product is a, up to units

theorem principal_ideal_ring.mem_submonoid_of_factors_subset_of_units_subset {R : Type u} [integral_domain R] [is_principal_ideal_ring R] (s : submonoid R) {a : R} (ha : a 0) (hfac : ∀ (b : R), b principal_ideal_ring.factors ab s) (hunit : ∀ (c : units R), c s) :
a s

theorem principal_ideal_ring.ring_hom_mem_submonoid_of_factors_subset_of_units_subset {R : Type u_1} {S : Type u_2} [integral_domain R] [is_principal_ideal_ring R] [semiring S] (f : R →+* S) (s : submonoid S) (a : R) (ha : a 0) (h : ∀ (b : R), b principal_ideal_ring.factors af b s) (hf : ∀ (c : units R), f c s) :
f a s

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