[Merged by Bors] - feat(ValuationSubring): eq_self_or_eq_top_of_le by xgenereux · Pull Request #33634 · leanprover-community/mathlib4

xgenereux · 2026-01-05T22:35:51Z

Using primeSpectrumEquiv we get the the corresponding results of IsLocalRing.primeSpectrum_eq_of_KrullDimLEOne(see #33607) for valuation subrings.

Co-authored-by: María Inés de Frutos Fernández <[email protected]>

depends on: [Merged by Bors] - feat(ValuationSubring): simp lemmas for idealOfLE/ofPrime in relation to top/bot #33631
depends on: [Merged by Bors] - feat(ValuationSubring): fieldTop #33612
depends on: [Merged by Bors] - refactor: Ideal.bot_prime as an instance #33609
depends on: [Merged by Bors] - feat(Spectrum/Prime/Topology): Ring.KrullDimLE.eq_bot_or_eq_top #33607

github-actions · 2026-01-05T22:37:07Z

PR summary 5833ef5cdf

Import changes exceeding 2%

%	File
+28.90%	`Mathlib.RingTheory.Valuation.ValuationSubring`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Valuation.ValuationSubring	1377	1775	+398 (+28.90%)

Import changes for all files

Files	Import difference
25 files `Mathlib.Analysis.Fourier.ZMod` `Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar` `Mathlib.NumberTheory.DirichletCharacter.GaussSum` `Mathlib.NumberTheory.Fermat` `Mathlib.NumberTheory.GaussSum` `Mathlib.NumberTheory.Height.NumberField` `Mathlib.NumberTheory.JacobiSum.Basic` `Mathlib.NumberTheory.LSeries.DirichletContinuation` `Mathlib.NumberTheory.LSeries.Nonvanishing` `Mathlib.NumberTheory.LSeries.PrimesInAP` `Mathlib.NumberTheory.LSeries.ZMod` `Mathlib.NumberTheory.LegendreSymbol.AddCharacter` `Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol` `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum` `Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity` `Mathlib.NumberTheory.LucasLehmer` `Mathlib.NumberTheory.MahlerMeasure` `Mathlib.NumberTheory.NumberField.AdeleRing` `Mathlib.NumberTheory.NumberField.CMField` `Mathlib.NumberTheory.NumberField.Completion.FinitePlace` `Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings` `Mathlib.NumberTheory.NumberField.FinitePlaces` `Mathlib.NumberTheory.NumberField.ProductFormula` `Mathlib.Tactic.NormNum.LegendreSymbol` `Mathlib.Tactic`	18
30 files `Mathlib.AlgebraicGeometry.EllipticCurve.Reduction` `Mathlib.FieldTheory.Laurent` `Mathlib.FieldTheory.RatFunc.AsPolynomial` `Mathlib.FieldTheory.RatFunc.Degree` `Mathlib.FieldTheory.RatFunc.Luroth` `Mathlib.NumberTheory.ClassNumber.FunctionField` `Mathlib.NumberTheory.Cyclotomic.Basic` `Mathlib.NumberTheory.Cyclotomic.Discriminant` `Mathlib.NumberTheory.Cyclotomic.Gal` `Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots` `Mathlib.NumberTheory.FunctionField` `Mathlib.NumberTheory.NumberField.Cyclotomic.Galois` `Mathlib.NumberTheory.Padics.HeightOneSpectrum` `Mathlib.NumberTheory.PrimesCongruentOne` `Mathlib.RingTheory.DedekindDomain.AdicValuation` `Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing` `Mathlib.RingTheory.DedekindDomain.GaussLemma` `Mathlib.RingTheory.DedekindDomain.SInteger` `Mathlib.RingTheory.DedekindDomain.SelmerGroup` `Mathlib.RingTheory.LaurentSeries` `Mathlib.RingTheory.LittleWedderburn` `Mathlib.RingTheory.Polynomial.Cyclotomic.Basic` `Mathlib.RingTheory.Polynomial.Cyclotomic.Eval` `Mathlib.RingTheory.Polynomial.Cyclotomic.Expand` `Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization` `Mathlib.RingTheory.Polynomial.Cyclotomic.Roots` `Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral` `Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed` `Mathlib.RingTheory.Valuation.Discrete.Basic` `Mathlib.RingTheory.Valuation.Discrete.RankOne`	22
3 files `Mathlib.NumberTheory.Padics.Complex` `Mathlib.NumberTheory.Padics.WithVal` `Mathlib.Topology.Algebra.Valued.WithVal`	29
`Mathlib.RingTheory.Valuation.LocalSubring`	116
`Mathlib.RingTheory.Valuation.AlgebraInstances`	138
`Mathlib.NumberTheory.LocalField.Basic` `Mathlib.Topology.Algebra.Valued.LocallyCompact`	218
`Mathlib.Topology.Algebra.Valued.NormedValued`	223
`Mathlib.Topology.Algebra.Valued.WithZeroMulInt`	294
`Mathlib.Analysis.Real.Hyperreal`	310
`Mathlib.Algebra.Order.Ring.StandardPart` `Mathlib.Topology.Algebra.Valued.ValuedField`	311
`Mathlib.Topology.Algebra.Valued.ValuativeRel`	312
`Mathlib.Topology.Algebra.Valued.ValuationTopology`	313
`Mathlib.RingTheory.Valuation.Extension`	397
`Mathlib.RingTheory.Valuation.RamificationGroup` `Mathlib.RingTheory.Valuation.ValuationSubring`	398

Declarations diff

+ eq_of_le_of_ne_self
+ eq_of_le_of_ne_top
+ eq_of_lt
+ eq_self_or_eq_top_of_le

You can run this locally as follows

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh 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).

xgenereux · 2026-01-05T22:45:24Z

Question:
For the large import should I:

make a ValuationSubring folder
current file would be basic
make a new file for this result (maybe called KrullDimLEOne?)

Or is it fine like this?

Thanks!

misclick

mathlib4-merge-conflict-bot · 2026-01-13T21:29:29Z

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

mathlib-dependent-issues · 2026-03-16T19:10:50Z

This PR/issue depends on:

~~[Merged by Bors] - feat(ValuationSubring): simp lemmas for idealOfLE/ofPrime in relation to top/bot #33631~~
~~[Merged by Bors] - feat(ValuationSubring): fieldTop #33612~~
~~[Merged by Bors] - refactor: Ideal.bot_prime as an instance #33609~~
~~[Merged by Bors] - feat(Spectrum/Prime/Topology): Ring.KrullDimLE.eq_bot_or_eq_top #33607~~
By Dependent Issues (🤖). Happy coding!

xgenereux · 2026-03-24T14:18:38Z

!bench

xgenereux · 2026-03-24T14:18:57Z

Checking if the large import is an issue.

leanprover-radar · 2026-03-24T14:19:10Z

Benchmark results for 391223c against 5833ef5 are in. Significant changes detected! @xgenereux

✅ build//instructions: -6.8G (-0.00%)

Small changes (1✅, 20🟥)

Too many entries to display here. View the full report on radar instead.

dagurtomas

Thanks!

maintainer delegate

dagurtomas · 2026-03-26T20:17:51Z

+  obtain h | h := IsLocalRing.Ring.KrullDimLE.eq_bot_or_eq_top
+    ((primeSpectrumEquiv A).symm ⟨B, hle⟩) <;>
+    (replace h := congr((primeSpectrumEquiv A) $h); simp_all [← idealOfLE_self])


Suggested change

obtain h | h := IsLocalRing.Ring.KrullDimLE.eq_bot_or_eq_top

((primeSpectrumEquiv A).symm ⟨B, hle⟩) <;>

(replace h := congr((primeSpectrumEquiv A) $h); simp_all [← idealOfLE_self])

obtain h | h := IsLocalRing.Ring.KrullDimLE.eq_bot_or_eq_top

((primeSpectrumEquiv A).symm ⟨B, hle⟩)

all_goals

replace h := congrArg (primeSpectrumEquiv A) h

simp_all

This is more readable

github-actions · 2026-03-26T20:19:10Z

🚀 Pull request has been placed on the maintainer queue by dagurtomas.

pull_request_review, wf_run

riccardobrasca · 2026-03-27T09:04:18Z

Thanks!

bors d+

mathlib-bors · 2026-03-27T09:04:20Z

✌️ xgenereux can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

xgenereux · 2026-03-27T15:56:53Z

bors r+

Using `primeSpectrumEquiv` we get the the corresponding results of `IsLocalRing.primeSpectrum_eq_of_KrullDimLEOne`(see #33607) for valuation subrings. Co-authored-by: María Inés de Frutos Fernández <[[email protected]](mailto:[email protected])> Co-authored-by: Xavier Genereux <[email protected]>

mathlib-bors · 2026-03-27T16:33:41Z

Pull request successfully merged into master.

Build succeeded:

…#33634) Using `primeSpectrumEquiv` we get the the corresponding results of `IsLocalRing.primeSpectrum_eq_of_KrullDimLEOne`(see leanprover-community#33607) for valuation subrings. Co-authored-by: María Inés de Frutos Fernández <[[email protected]](mailto:[email protected])> Co-authored-by: Xavier Genereux <[email protected]>

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Jan 5, 2026

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 5, 2026

xgenereux mentioned this pull request Jan 5, 2026

feat: localizations of primes in Dedekind domains are valuation subrings #33010

Open

2 tasks

plp127 reviewed Jan 5, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/Valuation/ValuationSubring.lean

alreadydone previously approved these changes Jan 10, 2026

View reviewed changes

mathlib4-merge-conflict-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 Jan 13, 2026

joneugster added the t-algebra Algebra (groups, rings, fields, etc) label Feb 1, 2026

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 Feb 7, 2026

mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 16, 2026

mathlib-dependent-issues bot deleted a comment from mathlib4-dependent-issues-bot Mar 16, 2026

xgenereux added 2 commits March 16, 2026 16:36

feat(ValuationSubring): eq_self_or_eq_top_of_le

f7c9ddb

update depr. decl

391223c

xgenereux force-pushed the ValuationSubring_dimLEOne branch from 38f340a to 391223c Compare March 16, 2026 20:39

mathlib-triage bot assigned dagurtomas Mar 20, 2026

dagurtomas reviewed Mar 26, 2026

View reviewed changes

mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Mar 26, 2026

mathlib-triage bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Mar 27, 2026

clean up

96da4c9

mathlib-bors bot changed the title ~~feat(ValuationSubring): eq_self_or_eq_top_of_le~~ [Merged by Bors] - feat(ValuationSubring): eq_self_or_eq_top_of_le Mar 27, 2026

mathlib-bors bot closed this Mar 27, 2026

Conversation

xgenereux commented Jan 5, 2026 • edited by riccardobrasca Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jan 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 5833ef5cdf

Import changes for modified files

Declarations diff

Uh oh!

xgenereux commented Jan 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

mathlib4-merge-conflict-bot commented Jan 13, 2026

Uh oh!

mathlib-dependent-issues bot commented Mar 16, 2026

Uh oh!

xgenereux commented Mar 24, 2026

Uh oh!

xgenereux commented Mar 24, 2026

Uh oh!

leanprover-radar commented Mar 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

dagurtomas left a comment

Choose a reason for hiding this comment

Uh oh!

dagurtomas Mar 26, 2026

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Mar 26, 2026

Uh oh!

riccardobrasca commented Mar 27, 2026

Uh oh!

mathlib-bors bot commented Mar 27, 2026

Uh oh!

xgenereux commented Mar 27, 2026

Uh oh!

mathlib-bors bot commented Mar 27, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

9 participants

xgenereux commented Jan 5, 2026 •

edited by riccardobrasca

Loading

github-actions bot commented Jan 5, 2026 •

edited

Loading

xgenereux commented Jan 5, 2026 •

edited

Loading

leanprover-radar commented Mar 24, 2026 •

edited

Loading