Commit 2025-04-07 16:44 f62f2aa9

feat(RingTheory): dim R + 1 ≤ dim R[X] (#21088) We add the following results

• ringKrullDim_quotient_succ_le_of_nonZeroDivisor: If r is not a zero divisor, then dim R/r + 1 ≤ dim R.
• ringKrullDim_succ_le_ringKrullDim_polynomial: dim R + 1 ≤ dim R[X].
• ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial: dim R + #σ ≤ dim R[σ].