Theorem ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_nonZeroDivisors

Modification history

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