Theorem ringKrullDim_quotSMulTop_succ_eq_ringKrullDim

Modification history

2025-12-09 05:22
Mathlib/RingTheory/KrullDimension/Regular.lean
feat(RingTheory): `ringKrullDim` of quotient via supportDim (#29937) …
Added ringKrullDim_quotSMulTop_succ_eq_ringKrullDimView on Github →