Commit 2025-11-10 13:35 b2847e75

feat(RingTheory/KrullDimension): Krull Dimension of quotient regular sequence (#26219) We show that if M is a finite module over a Noetherian local ring R, [r₁, …, rₙ] is an M-sequence, then dim M⧸(r₁, …, rₙ)M + n = dim M.