[Merged by Bors] - chore: make FiniteAdeleRing a def rather than an abbrev

[kbuzzard]

On current master #synth CommRing (FiniteAdeleRing A K) works fine but #synth SMul (FiniteAdeleRing A K) (FiniteAdeleRing A K) times out because typeclass inference can see through the abbrev and the first thing it tries is "if G acts on X_i for all i then G acts on the restricted product" and it goes off on a wild goose chase, quickly hitting dreaded stuff such as [] ✅️ apply @NormedAlgebra.toAlgebra to Algebra (FiniteAdeleRing A K) K ▶ , spending a long time failing on Group (FiniteAdeleRing A K) and so on. I claim that there is no need for typeclass inference to know that finite adele rings are actually restricted products; this is in some sense an implentation detail (the finite adele ring of a number field $K$ is just $K\otimes_{\mathbb{Z}}\widehat{\mathbb{Z}}$; the fact that we represent it as a restricted product is some sense a historical coincidence). Indeed, we have developed the theory of adeles and finite adeles a lot further in the FLT repo and there is only one place where we had an auxiliary restricted product of vector spaces and used typeclass inference to give a module structure over a finite adele ring; this was some internal object in a proof.

---

[github-actions]

PR summary a86aa1d39e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ instance : CommRing (FiniteAdeleRing R K) := inferInstanceAs <|
+ instance : DFunLike (FiniteAdeleRing R K) (HeightOneSpectrum R) (fun v ↦ v.adicCompletion K)
+ instance : TopologicalSpace (FiniteAdeleRing R K) := inferInstanceAs <|

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

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

[kbuzzard]

!bench

[leanprover-radar]

Benchmark results for ae61f3e against 9649952 are in! @kbuzzard

Major changes (1)

• ✅ build/module/Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing//instructions: -11.6G (-39.0%) from estimate, -9.5G (-34.3%) from previous value

Minor changes (1)

• ✅ build/module/Mathlib.NumberTheory.NumberField.AdeleRing//instructions: -5.6G (-22.9%)

[leanprover-bot]

Here are the benchmark results for commit ae61f3e.
There were no significant changes against commit 9649952.

[github-actions]

File	Instructions	%
build	-27.256⬝10⁹	(-0.01%)
lint	-1.67⬝10⁹	(-0.01%)
Mathlib.Analysis.Asymptotics.LinearGrowth	+1.187⬝10⁹	(+2.95%)

4 files, Instructions -2.0⬝10⁹

File	Instructions	%
Mathlib.LinearAlgebra.TensorProduct.Tower	-1.59⬝10⁹	(-0.51%)
Mathlib.Tactic.NormNum.Pow	-1.102⬝10⁹	(-5.64%)
Mathlib.Algebra.Polynomial.Eval.SMul	-1.274⬝10⁹	(-15.31%)
Mathlib.AlgebraicGeometry.GammaSpecAdjunction	-1.402⬝10⁹	(-1.72%)

File	Instructions	%
Mathlib.NumberTheory.NumberField.AdeleRing	-5.468⬝10⁹	(-23.90%)
Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing	-9.491⬝10⁹	(-36.00%)
CI run Lakeprof report

[kbuzzard]

After seeing the benchmarking, I think that hiding the implementation of FiniteAdeleRing and duplicating API makes the world a better place. The definition of FiniteAdeleRing as a restricted product is not really "used", what we seem to use in practice is the K-algebra structure, the topological ring structure and the fact that there's a coercion to a dependent function sending a valuation to the coefficient of the adele at that valuation. In FLT I use a little more but I can add the extra API when upstreaming.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Build failed (retrying...):

• Post-Build Step

[mathlib-bors]

Build failed (retrying...):

• Post-Build Step

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Post-Build Step
• Lint style