Theorem ringKrullDim_le_ringKrullDim_quotSMulTop_succ

Modification history

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