Principal ideal domains and prime ideals #
Main results #
IsPrincipalIdeal.of_prime: a ring where all prime ideals are principal is a principal ideal ring
theorem
IsPrincipalIdealRing.of_prime
{R : Type u_1}
[CommRing R]
(H : ∀ (P : Ideal R), P.IsPrime → Submodule.IsPrincipal P)
:
If all prime ideals in a commutative ring are principal, so are all other ideals.