Commit 2026-01-10 16:04 9196e9f9

View on Github →

feat(RingTheory/KrullDimension): dimension of polynomial ring (#27542) We show that for a Noetherian ring R, dim R[X] = dim R + 1. Co-authored by: Sihan Su ssh@stu.pku.edu.cn Co-authored by: Yi Song sif4delta0@mail.ustc.edu.cn

Estimated changes

Modified Mathlib/Order/KrullDimension.lean

added theorem Order.coheight_pos_of_lt_top

added theorem Order.height_pos_of_bot_lt

Modified Mathlib/RingTheory/Ideal/Height.lean

added theorem IsLocalization.height_map_of_disjoint

Modified Mathlib/RingTheory/KrullDimension/Polynomial.lean

added theorem MvPolynomial.ringKrullDim_of_isNoetherianRing

added theorem Polynomial.height_eq_height_add_one

added theorem Polynomial.height_map_C

added theorem Polynomial.ringKrullDim_of_isNoetherianRing

Modified Mathlib/RingTheory/Localization/AtPrime/Basic.lean

added theorem Ideal.IsMaximal.of_isLocalization_of_disjoint

added theorem IsLocalization.liesOver_of_isPrime_of_disjoint