[Merged by Bors] - refactor(NumberTheory): make `adicCompletion` a one-field structure by smmercuri · Pull Request #41526 · leanprover-community/mathlib4

smmercuri · 2026-07-09T07:00:46Z

adicCompletion as an abbrev is causing slowdown in FLT.

smmercuri · 2026-07-09T07:01:00Z

!radar

leanprover-radar · 2026-07-09T07:01:20Z

Benchmark results for dd1384c against 6f60478 are in. There are significant results. @smmercuri

🟥 main exited with code 1

No significant changes detected.

github-actions · 2026-07-09T07:02:16Z

PR summary 1894d7061c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff (regex)

+ algebraMap_adicCompletion_toCompletion
+ coe_add
+ coe_mul
+ coe_one
+ coe_toCompletion
+ coe_valueGroupEquiv
+ coe_valueGroupOrderIso_coe
+ coe_zero
+ continuous_ofCompletion
+ continuous_toCompletion
+ embedding_valueGroupOrderIso
+ equiv
+ equivCompletion
+ ext
+ instAlgebraCompletion
+ instance (priority := 99) : Coe K (adicCompletion K v)
+ instance : Coe (WithVal (v.valuation K)) (adicCompletion K v)
+ instance : CompleteSpace (adicCompletion K v)
+ instance : Field (adicCompletion K v) := fast_instance% (equivCompletion K v).field
+ instance : IsUniformAddGroup (adicCompletion K v)
+ instance : T0Space (adicCompletion K v)
+ instance : UniformSpace (adicCompletion K v) := .comap toCompletion inferInstance
+ instance : Valued (adicCompletion K v) ℤᵐ⁰
+ isUniformInducing_toCompletion
+ ofCompletion_surjective
+ ofCompletion_toCompletion
+ toCompletion_add
+ toCompletion_mul
+ toCompletion_ofCompletion
+ toCompletion_one
+ toCompletion_surjective
+ toCompletion_zero
+ uniformEquiv
+ valuation
+ valueGroupEquiv
+ valueGroupOrderIso
+ valueGroupOrderIso_restrict
+ valueGroup_eq
+ valued_coe
+ valued_ofCompletion
+ valued_toCompletion
++ instance {S₀ : Type*} [CommSemiring S₀] [Algebra S₀ S] [Algebra S₀ K] [IsScalarTower S₀ S K] :

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 1894d70).

+60 new declarations
−3 removed declarations

+IsDedekindDomain.HeightOneSpectrum.adicCompletion.casesOn
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_add
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_mul
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_one
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_toCompletion
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_valueGroupEquiv
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_valueGroupOrderIso_coe
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_zero
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.continuous_ofCompletion
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.continuous_toCompletion
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.ctorIdx
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.embedding_valueGroupOrderIso
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.equiv
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.equivCompletion
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.equivCompletion_apply
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.equivCompletion_symm_apply_toCompletion
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.equiv_apply
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext_iff
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.instCoe
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.instCoeWithValWithZeroMultiplicativeIntValuation
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.instCompleteSpace
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.instField
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsUniformAddGroup
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.instT0Space
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.instUniformSpace
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.instValuedWithZeroMultiplicativeInt
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.isUniformInducing_toCompletion
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.noConfusion
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.noConfusionType
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion.inj
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion.injEq
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion.noConfusion
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion.sizeOf_spec
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion_surjective
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion_toCompletion
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.rec
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.recOn
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_add
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_mul
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_ofCompletion
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_one
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_surjective
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_zero
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.uniformEquiv
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuation
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupEquiv
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderIso
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderIso_restrict
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroup_eq
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuedAdicCompletion_def
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_coe
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_ofCompletion
+IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_toCompletion
+IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion_toCompletion
+IsDedekindDomain.HeightOneSpectrum.instAlgebraCompletion
+IsDedekindDomain.HeightOneSpectrum.instIsScalarTowerAdicCompletion
+IsDedekindDomain.HeightOneSpectrum.instIsScalarTowerCompletionWithZeroMultiplicativeIntValuation
-IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def
-LaurentSeries.extensionAsRingHom.congr_simp
-UniformSpace.Completion.instField.congr_simp

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 1894d7061c
Reference commit 2d00c9242a

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

smmercuri · 2026-07-09T09:10:41Z

!radar

leanprover-radar · 2026-07-09T09:10:59Z

Benchmark results for a7bd575 against 6f60478 are in. There are significant results. @smmercuri

✅ build//instructions: -121.7G (-0.08%)

Large changes (2✅)

✅ build/module/Mathlib.NumberTheory.NumberField.Completion.FinitePlace//instructions: -20.9G (-35.50%)
✅ build/module/Mathlib.RingTheory.LaurentSeries//instructions: -26.7G (-17.12%)

Medium changes (2✅)

✅ build/module/Mathlib.NumberTheory.Padics.HeightOneSpectrum//instructions: -5.2G (-10.72%)
✅ build/module/Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing//instructions: -7.4G (-32.43%)

Small changes (1🟥)

🟥 build/module/Mathlib.RingTheory.DedekindDomain.AdicValuation//instructions: +66.5G (+69.97%) (reduced significance based on *//lines)

YaelDillies

Thanks! 🚀

maintainer merge

github-actions · 2026-07-09T10:14:59Z

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

riccardobrasca · 2026-07-09T11:27:14Z

Thanks!

bors d+

mathlib-bors · 2026-07-09T11:27:18Z

✌️ smmercuri can now approve this pull request until 2026-07-23 11:27 UTC (in 2 weeks). To approve and merge, reply with bors r+. More detailed instructions are available here.

⚠️ This delegation only covers changes within Archive/**, Counterexamples/**, docs/**, DownstreamTest/**, Mathlib/**, MathlibTest/**, widget/**, Archive.lean, Counterexamples.lean, docs.lean, Mathlib.lean; an author commit touching anything else will revoke it. Bors also revokes it if a later push changes too many files for it to check the full list — even if it stays within scope.

…dicCompletion-one-field

smmercuri · 2026-07-09T14:12:58Z

bors r+

…41526) `adicCompletion` as an `abbrev` is causing slowdown in FLT.

mathlib-bors · 2026-07-09T14:40:01Z

Pull request successfully merged into master.

Build succeeded:

- Bump to get [#41526](leanprover-community/mathlib4#41526) - Remove lots of instance hacks as a result

…eanprover-community#41526) `adicCompletion` as an `abbrev` is causing slowdown in FLT.

…tructure (#41543) Makes FLT a lot faster. `InfinitePlace` analogue of #41526.

smmercuri added 2 commits July 8, 2026 16:47

draft

4b68f3a

one-field structure

dd1384c

smmercuri added the WIP Work in progress label Jul 9, 2026

simp -> norm_cast

a7bd575

smmercuri added 2 commits July 9, 2026 11:06

golf

6269124

golf

488bcf0

smmercuri removed the WIP Work in progress label Jul 9, 2026

YaelDillies changed the title ~~refactor: make adicCompletion a one-field structure~~ refactor(NumberTheory): make adicCompletion a one-field structure Jul 9, 2026

YaelDillies added the t-number-theory Number theory (also use t-algebra or t-analysis to specialize) label Jul 9, 2026

YaelDillies approved these changes Jul 9, 2026

View reviewed changes

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

riccardobrasca reviewed Jul 9, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/LaurentSeries.lean Outdated

revert comparePkg type

5bffbc3

mathlib-bors Bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jul 9, 2026

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

smmercuri added 2 commits July 9, 2026 13:35

Merge branch 'master' of https://github.com/smmercuri/mathlib4 into a…

f4e126b

…dicCompletion-one-field

Merge branch 'master' of https://github.com/smmercuri/mathlib4 into a…

1894d70

…dicCompletion-one-field

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

mathlib-bors Bot pushed a commit that referenced this pull request Jul 9, 2026

refactor(NumberTheory): make adicCompletion a one-field structure (#…

8bba420

…41526) `adicCompletion` as an `abbrev` is causing slowdown in FLT.

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

mathlib-bors Bot changed the title ~~refactor(NumberTheory): make adicCompletion a one-field structure~~ [Merged by Bors] - refactor(NumberTheory): make adicCompletion a one-field structure Jul 9, 2026

mathlib-bors Bot closed this Jul 9, 2026

mathlib-bors Bot removed the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jul 9, 2026

smmercuri mentioned this pull request Jul 9, 2026

bump to get the adicCompletion refactor ImperialCollegeLondon/FLT#1100

Merged

kbuzzard pushed a commit to ImperialCollegeLondon/FLT that referenced this pull request Jul 10, 2026

bump to get the adicCompletion refactor (#1100)

44df774

- Bump to get [#41526](leanprover-community/mathlib4#41526) - Remove lots of instance hacks as a result

smmercuri mentioned this pull request Jul 10, 2026

[Merged by Bors] - refactor(NumberTheory): make InfinitePlace.Completion a one-field structure #41543

Closed

michaellee94 pushed a commit to michaellee94/mathlib4 that referenced this pull request Jul 11, 2026

refactor(NumberTheory): make adicCompletion a one-field structure (l…

29d73c6

…eanprover-community#41526) `adicCompletion` as an `abbrev` is causing slowdown in FLT.

mathlib-bors Bot pushed a commit that referenced this pull request Jul 13, 2026

refactor(NumberTheory): make InfinitePlace.Completion a one-field s…

a3364fa

…tructure (#41543) Makes FLT a lot faster. `InfinitePlace` analogue of #41526.

Uh oh!

Conversation

smmercuri commented Jul 9, 2026 • edited by YaelDillies Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

smmercuri commented Jul 9, 2026

Uh oh!

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

Uh oh!

Uh oh!

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

Uh oh!

PR summary 1894d7061c

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

smmercuri commented Jul 9, 2026

Uh oh!

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

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions Bot commented Jul 9, 2026

Uh oh!

Uh oh!

riccardobrasca commented Jul 9, 2026

Uh oh!

mathlib-bors Bot commented Jul 9, 2026

Uh oh!

smmercuri commented Jul 9, 2026

Uh oh!

mathlib-bors Bot commented Jul 9, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

smmercuri commented Jul 9, 2026 •

edited by YaelDillies

Loading

leanprover-radar commented Jul 9, 2026 •

edited

Loading

github-actions Bot commented Jul 9, 2026 •

edited

Loading

leanprover-radar commented Jul 9, 2026 •

edited

Loading