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

[smmercuri]

Makes FLT a lot faster. InfinitePlace analogue of #41526.

---

[smmercuri]

!radar

[leanprover-radar]

Benchmark results for b404b46 against 8bba420 are in. There are significant results. @smmercuri

• 🟥 build//instructions: +29.9G (+0.02%)

Large changes (2✅)

• ✅ build/module/Mathlib.NumberTheory.NumberField.Completion.InfinitePlace//instructions: -11.0G (-25.17%)
• ✅ build/module/Mathlib.NumberTheory.NumberField.Completion.Ramification//instructions: -23.0G (-61.08%)

Medium changes (2✅)

• ✅ build/module/Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances//instructions: -3.6G (-25.11%)
• ✅ build/module/Mathlib.NumberTheory.NumberField.InfiniteAdeleRing//instructions: -6.9G (-39.30%)

[github-actions]

PR summary 6bf2aabeb9

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ algebraMap_apply
+ algebraMap_toCompletion
+ coe_algebraMap
+ coe_toCompletion
+ completionMap
+ completionMap_coe
+ continuous_coe
+ continuous_completionMap
+ continuous_ofCompletion
+ continuous_toCompletion
+ denseRange_coe
+ equiv
+ equivCompletion
+ ext
+ induction_on
+ instance : Algebra R v.Completion := fast_instance% (equivCompletion v).algebra R
+ instance : Coe (WithAbs v.1) v.Completion
+ instance : Coe K v.Completion
+ instance : CompleteSpace v.Completion
+ instance : Inhabited v.Completion := ⟨0⟩
+ instance : NormedField v.Completion := fast_instance% (equivCompletion v).normedField
+ isometryEquivCompletion
+ isometry_toCompletion
+ norm_ofCompletion
+ norm_toCompletion
+ ofCompletion_surjective
+ ofCompletion_toCompletion
+ toCompletion_ofCompletion
+ toCompletion_surjective

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

• +47 new declarations
• −1 removed declarations

+NumberField.InfinitePlace.Completion.algebraMap_apply
+NumberField.InfinitePlace.Completion.algebraMap_toCompletion
+NumberField.InfinitePlace.Completion.casesOn
+NumberField.InfinitePlace.Completion.coe_algebraMap
+NumberField.InfinitePlace.Completion.coe_toCompletion
+NumberField.InfinitePlace.Completion.continuous_coe
+NumberField.InfinitePlace.Completion.continuous_ofCompletion
+NumberField.InfinitePlace.Completion.continuous_toCompletion
+NumberField.InfinitePlace.Completion.ctorIdx
+NumberField.InfinitePlace.Completion.denseRange_coe
+NumberField.InfinitePlace.Completion.equiv
+NumberField.InfinitePlace.Completion.equivCompletion
+NumberField.InfinitePlace.Completion.equivCompletion_apply
+NumberField.InfinitePlace.Completion.equivCompletion_symm_apply_toCompletion
+NumberField.InfinitePlace.Completion.equiv_apply
+NumberField.InfinitePlace.Completion.ext
+NumberField.InfinitePlace.Completion.ext_iff
+NumberField.InfinitePlace.Completion.induction_on
+NumberField.InfinitePlace.Completion.instAlgebra
+NumberField.InfinitePlace.Completion.instCoe
+NumberField.InfinitePlace.Completion.instCoeWithAbsRealValAbsoluteValueExistsRingHomComplexEqPlace
-NumberField.InfinitePlace.Completion.instCompletableTopFieldWithAbsRealValAbsoluteValueExistsRingHomComplexEqPlace
+NumberField.InfinitePlace.Completion.instCompleteSpace
+NumberField.InfinitePlace.Completion.instInhabited
+NumberField.InfinitePlace.Completion.instNormedField
+NumberField.InfinitePlace.Completion.isometryEquivCompletion
+NumberField.InfinitePlace.Completion.isometry_toCompletion
+NumberField.InfinitePlace.Completion.noConfusion
+NumberField.InfinitePlace.Completion.noConfusionType
+NumberField.InfinitePlace.Completion.norm_ofCompletion
+NumberField.InfinitePlace.Completion.norm_toCompletion
+NumberField.InfinitePlace.Completion.ofCompletion
+NumberField.InfinitePlace.Completion.ofCompletion.inj
+NumberField.InfinitePlace.Completion.ofCompletion.injEq
+NumberField.InfinitePlace.Completion.ofCompletion.noConfusion
+NumberField.InfinitePlace.Completion.ofCompletion.sizeOf_spec
+NumberField.InfinitePlace.Completion.ofCompletion_surjective
+NumberField.InfinitePlace.Completion.ofCompletion_toCompletion
+NumberField.InfinitePlace.Completion.rec
+NumberField.InfinitePlace.Completion.recOn
+NumberField.InfinitePlace.Completion.toCompletion
+NumberField.InfinitePlace.Completion.toCompletion_ofCompletion
+NumberField.InfinitePlace.Completion.toCompletion_surjective
+NumberField.InfinitePlace.instCompletableTopFieldWithAbsRealValAbsoluteValueExistsRingHomComplexEqPlace
+NumberField.LiesOver.completionMap
+NumberField.LiesOver.completionMap.congr_simp
+NumberField.LiesOver.completionMap_coe
+NumberField.LiesOver.continuous_completionMap

---

Decrease in strong tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (strong)
5619	-1	backward.isDefEq.respectTransparency

No changes to weak technical debt.

Current commit 6bf2aabeb9
Reference commit 8bba420098

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

[github-actions]

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

[kbuzzard]

LGTM!

maintainer merge (because the author is my post-doc)