Theorem IsSMulRegular.notMem_of_mem_minimalPrimes

Modification history

2025-11-10 13:35
Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean
feat(RingTheory/KrullDimension): Krull Dimension of quotient regular sequence (#26219) …
Added IsSMulRegular.notMem_of_mem_minimalPrimesView on Github →