The Krull dimension of a principal ideal domain #
In this file, we proved some results about the dimension of a principal ideal domain.
instance
IsPrincipalIdealRing.krullDimLE_one
(R : Type u_1)
[CommRing R]
[IsDomain R]
[IsPrincipalIdealRing R]
:
Ring.KrullDimLE 1 R
theorem
IsPrincipalIdealRing.ringKrullDim_eq_one
(R : Type u_1)
[CommRing R]
[IsDomain R]
[IsPrincipalIdealRing R]
(h : ¬IsField R)
: