Commit 2026-09-07 13:05 d3debb31

feat(RingTheory): krull dimension of a polynomial ring in an infinite number of variables (#41098) Add a simp lemma that dim(R[X_1, ...]) = ∞ and also derive an ENat-valued lemma that dim(R[X_s]) = dim(R) + card(X_s). Note that I keep the original lemma for finite index sets as @[simp] since this is likely to be the more common case in practice.