Tracking issue: dimension theory of (commutative) rings

The state of dimension theory in mathlib is very immature, but many things have been proven in various public or private repositories. This issue is meant to track the state of dimension theory and the road to mathlib.

Feel free to edit this issue to add projects you are aware of.

Completed or ongoing projects

• Krull's height theorem: done by @erdOne in this lean3 repository. A group of PKU students is working on porting it (see open PRs)
• Dimension of polynomial rings (also includes going-down and similar results): done by a group of PKU students here. This partly depends on Krull's height theorem.
• $$dim R/(x) + 1 \le dim R$$ for a non-zero divisor $$x$$: done by @erdOne (link?)
• Hilbert polynomials, Hilbert-Serre theorem: done by @jjaassoonn in #9819
• more on dimension theory done by @jjaassoonn in #6277

PRs

Port of Krull's height theorem

• #20744
• #20741
• #22236
• #21041
• #23778

General purpose preparations

• #20306
• #20725
• #21798
• #22300

This is a tracking issue rather than a self-contained task, and it names no target file or test. Start by reviewing the listed PRs and linked repositories to identify an unclaimed dimension-theory result with a defined scope. Done would require completing that separately scoped result and integrating its supporting work into mathlib.