Principal ideal domains and prime ideals

Main results

• IsPrincipalIdealRing.of_prime: a ring where all prime ideals are principal is a principal ideal ring.

theorem Ideal.isOka_isPrincipal {R : Type u_1} [CommSemiring R] : IsOka Submodule.IsPrincipal

Submodule.IsPrincipal is an Oka predicate.

theorem IsPrincipalIdealRing.of_prime {R : Type u_1} [CommSemiring R] (H : ∀ (P : Ideal R), P.IsPrime → Submodule.IsPrincipal P) : IsPrincipalIdealRing R

If all prime ideals in a commutative ring are principal, so are all other ideals.

theorem IsPrincipalIdealRing.of_prime_ne_bot {R : Type u_1} [CommSemiring R] (H : ∀ (P : Ideal R), P.IsPrime → P ≠ ⊥ → Submodule.IsPrincipal P) : IsPrincipalIdealRing R

If all prime ideals in a commutative ring that are not (0) are principal, so are all other ideals.