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] [IsPrincipalIdealRing R] : Ring.KrullDimLE 1 R

theorem IsPrincipalIdealRing.ringKrullDim_eq_one (R : Type u_1) [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] (h : ¬IsField R) : ringKrullDim R = 1

theorem IsPrincipalIdealRing.height_eq_one_of_isMaximal {R : Type u_1} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] (m : Ideal R) [m.IsMaximal] (h : ¬IsField R) : m.height = 1

In a PID that is not a field, every maximal ideal has height one.