[Merged by Bors] - feat(RingTheory): krull dimension of a polynomial ring in an infinite number of variables by vlad902 · Pull Request #41098 · leanprover-community/mathlib4

vlad902 · 2026-06-27T10:17:57Z

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.

github-actions · 2026-06-27T10:19:23Z

PR summary bc0d031df7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff (regex)

+ MvPolynomial.ringKrullDim_of_isNoetherianRing_of_finite
+ add_top_of_ne_bot
+ ringKrullDim_mvPolynomial_of_infinite
+ top_add_of_ne_bot

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit bc0d031).

+4 new declarations
−0 removed declarations

+MvPolynomial.ringKrullDim_of_isNoetherianRing_of_finite
+WithBot.add_top_of_ne_bot
+WithBot.top_add_of_ne_bot
+ringKrullDim_mvPolynomial_of_infinite

No changes to strong technical debt.
No changes to weak technical debt.

Current commit bc0d031df7
Reference commit 251e86bd1f

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

mathlib-merge-conflicts · 2026-07-08T22:46:15Z

This pull request has conflicts, please merge master and resolve them.

robin-carlier · 2026-09-05T10:27:25Z

Apart from the naming nitpick, LGTM!

… number of variables 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.

robin-carlier · 2026-09-06T09:36:40Z

Thanks!

maintainer merge

github-actions · 2026-09-06T09:37:07Z

🚀 Pull request has been placed on the maintainer queue by robin-carlier.

jcommelin

Thanks 🎉

bors merge

… 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.

mathlib-bors · 2026-09-07T13:05:18Z

Build failed (retrying...):

ci (staging) / Build

… 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.

mathlib-bors · 2026-09-07T13:23:36Z

Pull request successfully merged into master.

Build succeeded:

github-actions Bot added the t-ring-theory Ring theory label Jun 27, 2026

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 8, 2026

vlad902 force-pushed the krull-dim-infinite-mvpoly branch from 432b060 to b2717ba Compare July 9, 2026 07:01

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 9, 2026

vlad902 force-pushed the krull-dim-infinite-mvpoly branch from b2717ba to e3dd444 Compare August 1, 2026 08:02

vlad902 force-pushed the krull-dim-infinite-mvpoly branch from e3dd444 to a1c6ca5 Compare August 11, 2026 16:56

robin-carlier reviewed Sep 5, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/KrullDimension/NonZeroDivisors.lean Outdated

robin-carlier added the awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. label Sep 5, 2026

vlad902 force-pushed the krull-dim-infinite-mvpoly branch from a1c6ca5 to 8ce61eb Compare September 5, 2026 13:21

vlad902 removed the awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. label Sep 5, 2026

vlad902 added 3 commits September 5, 2026 15:45

Robin feedback

a5de220

Fix build failure by changing names

bc0d031

vlad902 force-pushed the krull-dim-infinite-mvpoly branch from 8ce61eb to bc0d031 Compare September 5, 2026 14:57

mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Sep 6, 2026

jcommelin reviewed Sep 7, 2026

View reviewed changes

mathlib-bors Bot added the ready-to-merge This PR has been sent to bors. label Sep 7, 2026

mathlib-triage Bot removed the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Sep 7, 2026

mathlib-bors Bot added the bors-staging This PR is currently being built by bors on the staging branch. label Sep 7, 2026

mathlib-bors Bot removed the bors-staging This PR is currently being built by bors on the staging branch. label Sep 7, 2026

mathlib-bors Bot added the bors-staging This PR is currently being built by bors on the staging branch. label Sep 7, 2026

mathlib-bors Bot changed the title ~~feat(RingTheory): krull dimension of a polynomial ring in an infinite number of variables~~ [Merged by Bors] - feat(RingTheory): krull dimension of a polynomial ring in an infinite number of variables Sep 7, 2026

mathlib-bors Bot closed this Sep 7, 2026

Navigation Menu

Uh oh!

[Merged by Bors] - feat(RingTheory): krull dimension of a polynomial ring in an infinite number of variables - #41098

[Merged by Bors] - feat(RingTheory): krull dimension of a polynomial ring in an infinite number of variables#41098
vlad902 wants to merge 3 commits into
leanprover-community:masterfrom
vlad902:krull-dim-infinite-mvpoly

vlad902 commented Jun 27, 2026

Uh oh!

github-actions Bot commented Jun 27, 2026 •

edited

Loading

Declarations diff (regex)

Uh oh!

mathlib-merge-conflicts Bot commented Jul 8, 2026

Uh oh!

Uh oh!

robin-carlier commented Sep 5, 2026

Uh oh!

robin-carlier commented Sep 6, 2026

Uh oh!

github-actions Bot commented Sep 6, 2026

Uh oh!

jcommelin left a comment

Uh oh!

mathlib-bors Bot commented Sep 7, 2026

Uh oh!

mathlib-bors Bot commented Sep 7, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

vlad902 commented Jun 27, 2026

Uh oh!

github-actions Bot commented Jun 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary bc0d031df7

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

mathlib-merge-conflicts Bot commented Jul 8, 2026

Uh oh!

Uh oh!

robin-carlier commented Sep 5, 2026

Uh oh!

robin-carlier commented Sep 6, 2026

Uh oh!

github-actions Bot commented Sep 6, 2026

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors Bot commented Sep 7, 2026

Uh oh!

mathlib-bors Bot commented Sep 7, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

github-actions Bot commented Jun 27, 2026 •

edited

Loading