Theorem ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobson

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_ringKrullDim_of_mem_jacobsonView on Github →