Commit 2025-06-04 12:09 aa2486c2

View on Github →

feat(RingTheory/Dimension): Upper bound of dimension of polynomial ring (#25201) In this PR, we proved the following proof_wanted in Mathlib.RingTheory.KrullDimension.Basic: For a commutative ring $R$, $dim R[X] \le 2 * dim R + 1$.

proof_wanted Polynomial.ringKrullDim_le :
    ringKrullDim (Polynomial R) ≤ 2 * (ringKrullDim R) + 1

Estimated changes

added theorem Ring.krullDimLE_iff