Theorem Ideal.IsMaximal.mem_associatedPrimes_of_isFractionRing

Modification history

2025-10-25 18:20
Mathlib/RingTheory/Ideal/AssociatedPrime/Finiteness.lean
feat(RingTheory): Noetherian ring of fractions is semilocal (#30837) …
Added Ideal.IsMaximal.mem_associatedPrimes_of_isFractionRingView on Github →