Theorem Module.ringKrullDim_quotient_add_one_of_mem_nonZeroDivisors

Modification history

2026-01-22 07:06
Mathlib/RingTheory/KrullDimension/Regular.lean
feat(RingTheory/KrullDimension): generalize some results about local rings (#27557) …
Added Module.ringKrullDim_quotient_add_one_of_mem_nonZeroDivisorsView on Github →