Commit 2025-10-06 17:04 f4f1bfc2

View on Github →

feat(RingTheory/Noetherian): add IsNoetherianRing.of_prime (#28451) This PR introduces the first usage of Ideal.IsOka introduced in #27200 to prove that if all prime ideals of a CommRing are finitely generated then this ring is Noetherian. To do so, we also added the lemma Ideal.mem_span_range_self.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/Ideal/Span.lean

added theorem Ideal.mem_span_range_self

modified theorem Ideal.span_pair_eq_span_left_iff_dvd

modified theorem Ideal.span_pair_eq_span_right_iff_dvd

Created Mathlib/RingTheory/Noetherian/OfPrime.lean

added theorem Ideal.isOka_fg

added theorem IsNoetherianRing.of_prime

Modified docs/references.bib