feat: the adele ring of a number field is locally compact

[smmercuri]

---

• depends on: feat: the finite adele ring is locally compact if each of the ring of integers is compact #21158
• depends on: feat: v.adicCompletionIntegers K is compact #21847

[github-actions]

PR summary d25149695c

Import changes exceeding 2%

%	File
+6.95%	Mathlib.RingTheory.DedekindDomain.AdicValuation
+6.93%	Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.DedekindDomain.AdicValuation	1597	1708	+111 (+6.95%)
Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing	1601	1712	+111 (+6.93%)
Mathlib.NumberTheory.NumberField.AdeleRing	2534	2542	+8 (+0.32%)

Import changes for all files

Files	Import difference
Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.NumberTheory.NumberField.ProductFormula	4
6 files Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.NumberTheory.Cyclotomic.Three Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.NumberField.AdeleRing	8
28 files Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.NumberTheory.ClassNumber.FunctionField Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.NumberTheory.Fermat Mathlib.NumberTheory.GaussSum 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.PrimesCongruentOne Mathlib.RingTheory.LittleWedderburn Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.RingTheory.Polynomial.Cyclotomic.Expand Mathlib.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Tactic	11
Mathlib.RingTheory.Polynomial.Cyclotomic.Basic	13
Mathlib.RingTheory.LaurentSeries	105
Mathlib.NumberTheory.FunctionField	109
Mathlib.RingTheory.DedekindDomain.SelmerGroup	110
6 files Mathlib.FieldTheory.Laurent Mathlib.FieldTheory.RatFunc.AsPolynomial Mathlib.FieldTheory.RatFunc.Degree Mathlib.RingTheory.DedekindDomain.AdicValuation Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.RingTheory.DedekindDomain.SInteger	111
Mathlib.Topology.Algebra.Valued.WithZeroMulInt (new file)	1498

---

Declarations diff

+ AdicCompletion.dvd_of_valued_le
+ AdicCompletion.exists_nonZeroDivisor_finset_valued_lt
+ AdicCompletion.exists_nonZeroDivisor_valued_lt
+ AdicCompletion.valued_eq_intValuationDef
+ AdicCompletion.valued_le_one
+ AdicCompletion.valued_ne_zero
+ Quotient.mk_out
+ Quotient.out_sub
+ adicCompletion.residueField_finite
+ algebraMap_image_mem_nhds
+ algebraMap_inducing
+ algebraMap_range_isCompact
+ algebraMap_range_mem_nhds
+ dvd_of_valued_lt
+ exists_pow_lt_of_le_neg_one
+ finite_cover_of_uniformity_basis
+ instLocallyCompactSpace
+ instance : CompactSpace (v.adicCompletionIntegers K)
+ instance : IsDiscreteValuationRing (v.adicCompletionIntegers K) := sorry
+ instance [NumberField K] : LocallyCompactSpace (AdeleRing R K)
+ instance [NumberField K] : LocallyCompactSpace (InfiniteAdeleRing K)
+ intValuation_uniformizer_ne_zero
+ integers_compactSpace
+ integers_isClosed
+ irreducible_valuation_le_ofAdd_neg_one
+ irreducible_valuation_lt_one
+ le_ofAdd_iff
+ le_ofAdd_of_toAdd_unzero_le
+ lt_ofAdd_iff
+ lt_ofAdd_of_toAdd_unzero_lt
+ mem_maximalIdeal_pow_valuation
+ mem_nhds_comap_algebraMap
+ mul_integer_apply
+ tendsto_zero_pow_of_le_neg_one
+ toAdd_unzero_le_of_lt_ofAdd
+ toAdd_unzero_lt_of_lt_ofAdd
+ units_toAdd_le_of_le
++ algebraMap_apply
++ algebraMap_injective
- locallyCompactSpace

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

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat: the finite adele ring is locally compact if each of the ring of integers is compact #21158
• feat: v.adicCompletionIntegers K is compact #21847
  By Dependent Issues (🤖). Happy coding!