Theorem MvPolynomial.ringKrullDim_of_isNoetherianRing

Modification history

2026-09-07 13:05
Mathlib/RingTheory/KrullDimension/Polynomial.lean
feat(RingTheory): krull dimension of a polynomial ring in an infinite number of variables (#41098) …
Modified MvPolynomial.ringKrullDim_of_isNoetherianRingView on Github →
2026-01-10 16:04
Mathlib/RingTheory/KrullDimension/Polynomial.lean
feat(RingTheory/KrullDimension): dimension of polynomial ring (#27542) …
Added MvPolynomial.ringKrullDim_of_isNoetherianRingView on Github →