Theorem IsNoetherianRing.exists_relSeries_isQuotientEquivQuotientPrime

Modification history

2025-05-03 07:23
Mathlib/RingTheory/Ideal/AssociatedPrime/Finiteness.lean
feat(Algebra): finiteness of associated primes (#24242) …
Added IsNoetherianRing.exists_relSeries_isQuotientEquivQuotientPrimeView on Github →