feat: v.adicCompletionIntegers K is compact

[smmercuri]

---

• depends on: feat: the ring of integers of a ℤₘ₀-valued field is compact whenever it is a DVR and the residue field is finite #21844
• depends on: [Merged by Bors] - feat: apply and coe results for UniformSpace.Completion.mapRingHom #24872

[github-actions]

PR summary cebd76422f

Import changes exceeding 2%

%	File
+6.58%	Mathlib.RingTheory.DedekindDomain.AdicValuation
+6.57%	Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.DedekindDomain.AdicValuation	1778	1895	+117 (+6.58%)
Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing	1781	1898	+117 (+6.57%)
Mathlib.NumberTheory.NumberField.AdeleRing	2600	2610	+10 (+0.38%)

Import changes for all files

Files	Import difference
Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.NumberTheory.NumberField.ProductFormula	6
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	10
29 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.Basic 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	14
Mathlib.RingTheory.LaurentSeries	111
Mathlib.FieldTheory.Laurent	115
Mathlib.RingTheory.DedekindDomain.SelmerGroup	116
6 files Mathlib.FieldTheory.RatFunc.AsPolynomial Mathlib.FieldTheory.RatFunc.Degree Mathlib.NumberTheory.FunctionField Mathlib.RingTheory.DedekindDomain.AdicValuation Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.RingTheory.DedekindDomain.SInteger	117
Mathlib.Topology.Algebra.Valued.WithZeroMulInt (new file)	1542

---

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
+ algebraMap_apply
+ algebraMap_image_mem_nhds
+ algebraMap_inducing
+ algebraMap_injective
+ algebraMap_mem_integers
+ algebraMap_range_isCompact
+ algebraMap_range_mem_nhds
+ comap
+ compactSpace_integers
+ dvd_of_valued_lt
+ exists_pow_lt_of_le_neg_one
+ finite_cover_of_uniformity_basis
+ instLocallyCompactSpace
+ instance (hwv : w.comap A = v) : Algebra (v.adicCompletion K) (w.adicCompletion L)
+ instance : Algebra 𝒪[(w.comap A).adicCompletion K] 𝒪[w.adicCompletion L]
+ instance : IsDiscreteValuationRing 𝒪[v.adicCompletion K] := sorry
+ instance : IsLocalHom (algebraMap 𝒪[(w.comap A).adicCompletion K] 𝒪[w.adicCompletion L])
+ instance : Module.Finite 𝒪[(w.comap A).adicCompletion K] 𝒪[w.adicCompletion L]
+ instance [NumberField K] : LocallyCompactSpace (AdeleRing R K)
+ instance [NumberField K] : LocallyCompactSpace (InfiniteAdeleRing K)
+ intValuation_uniformizer_ne_zero
+ integer_compactSpace
+ integer_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
+ mapRingHom_apply
+ mapRingHom_coe
+ mem_maximalIdeal_pow_valuation
+ mem_nhds_comap_algebraMap
+ out_sub
+ residueField_finite
+ tendsto_zero_pow_of_le_neg_one
+ toAdd_unzero_le_of_lt_ofAdd
+ toAdd_unzero_lt_of_lt_ofAdd
+ uniformContinuous_algebraMap
+ units_toAdd_le_of_le
+ valuation_comap
- 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).

[leanprover-community-bot-assistant]

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

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat: the ring of integers of a ℤₘ₀-valued field is compact whenever it is a DVR and the residue field is finite #21844
• [Merged by Bors] - feat: apply and coe results for UniformSpace.Completion.mapRingHom #24872
  By Dependent Issues (🤖). Happy coding!