Commit 2025-12-09 05:22 0806ad5e

View on Github →

feat(RingTheory): ringKrullDim of quotient via supportDim (#29937) In this PR, we establish some lemma about ringKrullDim of quotient via lemmas of supportDim.

Estimated changes

Modified Mathlib/RingTheory/KrullDimension/Regular.lean

added theorem ringKrullDim_le_ringKrullDim_add_card

added theorem ringKrullDim_le_ringKrullDim_add_spanFinrank

added theorem ringKrullDim_le_ringKrullDim_quotSMulTop_succ

added theorem ringKrullDim_quotSMulTop_succ_eq_ringKrullDim

added theorem ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobson