Noetherian rings and prime ideals

Main results

• IsNoetherianRing.of_prime: a ring where all prime ideals are finitely generated is a noetherian ring

References

• [cohen1950]: Commutative rings with restricted minimum condition, I. S. Cohen, Theorem 2

theorem Ideal.isOka_fg {R : Type u_1} [CommRing R] : IsOka FG

Ideal.FG is an Oka predicate.

theorem IsNoetherianRing.of_prime {R : Type u_1} [CommRing R] (H : ∀ (I : Ideal R), I.IsPrime → I.FG) : IsNoetherianRing R

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