Infinite.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

24 declarations, 0 contain sorry, 0 declared as axioms

The completion of a number field at an infinite place

Imports (15)

Imported by 2 files

instance NumberField.InfinitePlace.Completion.(instance at line 42) line 42 source
instance NumberField.InfinitePlace.Completion.(instance at line 45) line 45 source
instance NumberField.InfinitePlace.Completion.(instance at line 50) line 50 source
theorem NumberField.InfinitePlace.Completion.denseRange_algebraMap_subtype_pi line 54 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField.InfinitePlace, NumberField, DenseRange, Subtype, NumberField.InfinitePlace.Completion, RingHom, Algebra.algebraMap, Real, AbsoluteValue, Exists, Complex, Eq, NumberField.place
Proof uses: DenseRange.comp, Subtype.restrict, Function.Surjective.denseRange, Subtype.surjective_restrict, NumberField.InfiniteAdeleRing.denseRange_algebraMap, continuous_pi, continuous_apply
55 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
abbrev NumberField.InfinitePlace.Completion.comapHom The map from v.Completion to w.Completion whenever the infinite place w of L lies above the infinite place v of K line 64 source
Source documentation
The map from v.Completion to w.Completion whenever the infinite place w of L lies above the infinite place v of K.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace, Eq, NumberField.InfinitePlace.comap, Algebra.algebraMap, SemialgHom, NumberField.InfinitePlace.Completion, Real, AbsoluteValue, Exists, RingHom, Complex, NumberField.place
Proof uses: AbsoluteValue.LiesOver, RingHom.toSemialgHom, NumberField.LiesOver.completionMap
37 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
abbrev comapHom (h : w.comap (algebraMap K L) = v) :
    v.Completion →ₛₐ[algebraMap K L] w.Completion :=
…
```
theorem NumberField.InfinitePlace.Completion.comapHom_cont line 72 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace, Eq, NumberField.InfinitePlace.comap, Algebra.algebraMap, Continuous, NumberField.InfinitePlace.Completion, SemialgHom, Real, AbsoluteValue, Exists, RingHom, Complex, NumberField.place, NumberField.InfinitePlace.Completion.comapHom
Proof uses: AbsoluteValue.LiesOver, AbsoluteValue.LiesOver.mk, of_eq_true, AbsoluteValue.comp, FaithfulSMul.algebraMap_injective, Eq.trans, True, congrArg, Subtype.mk, Eq.symm, eq_self, NumberField.LiesOver.continuous_completionMap
47 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def NumberField.InfinitePlace.Completion.piExtension The map from v.Completion to the product of all completions of L lying above v line 79 source
Source documentation
The map from v.Completion to the product of all completions of L lying above v.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace, SemialgHom, Algebra.algebraMap, NumberField.InfinitePlace.Completion, NumberField.InfinitePlace.Extension, Eq, NumberField.InfinitePlace.comap, Real, AbsoluteValue, Exists, RingHom, Complex, NumberField.place
Proof uses: Pi.semialgHom, NumberField.InfinitePlace.Completion.comapHom
38 instances, coercions and auxiliary constants left out.
```
def piExtension :
    v.Completion →ₛₐ[algebraMap K L] (wv : v.Extension L) → wv.1.Completion :=
…
```
theorem NumberField.InfinitePlace.Completion.piExtension_apply line 84 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace, NumberField.InfinitePlace.Completion, Eq, NumberField.InfinitePlace.Extension, NumberField.InfinitePlace.comap, Algebra.algebraMap, SemialgHom, Real, AbsoluteValue, Exists, RingHom, Complex, NumberField.place, NumberField.InfinitePlace.Completion.piExtension, NumberField.InfinitePlace.Completion.comapHom, Subtype.property
Proof uses: rfl
44 instances, coercions and auxiliary constants left out.
instance NumberField.InfinitePlace.Completion.(instance at line 89) line 89 source
instance NumberField.InfinitePlace.Completion.(instance at line 91) line 91 source
abbrev NumberField.InfinitePlace.Completion.baseChange The L-algebra map L ⊗[K] v.Completion to the product of all completions of L lying above v, induced by piExtension line 95 source
Source documentation
The L-algebra map L ⊗[K] v.Completion to the product of all completions of L lying above v, induced by piExtension.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace, AlgHom, TensorProduct, NumberField.InfinitePlace.Completion, Real, AbsoluteValue, Exists, RingHom, Complex, Eq, NumberField.place, NumberField.InfinitePlace.Extension, NumberField.InfinitePlace.comap, Algebra.algebraMap
Proof uses: SemialgHom.baseChangeOfAlgebraMap, NumberField.InfinitePlace.Completion.piExtension
44 instances, coercions and auxiliary constants left out.
```
abbrev baseChange :
    L ⊗[K] v.Completion →ₐ[L] (wv : v.Extension L) → wv.1.Completion :=
…
```
abbrev NumberField.InfinitePlace.Completion.baseChangeRight The v.Completion-algebra map L ⊗[K] v.Completion to the product of all completions of L lying above v, induced by piExtension line 104 source
Source documentation
The v.Completion-algebra map L ⊗[K] v.Completion to the product of all completions of L lying above v, induced by piExtension.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace, AlgHom, NumberField.InfinitePlace.Completion, TensorProduct, Real, AbsoluteValue, Exists, RingHom, Complex, Eq, NumberField.place, NumberField.InfinitePlace.Extension, NumberField.InfinitePlace.comap, Algebra.algebraMap, TensorProduct.RightActions.instAlgebra_fLT, NumberField.LiesOver.instAlgebraCompletion
Proof uses: SemialgHom.baseChangeRightOfAlgebraMap, NumberField.InfinitePlace.Completion.piExtension
43 instances, coercions and auxiliary constants left out.
```
abbrev baseChangeRight :
    L ⊗[K] v.Completion →ₐ[v.Completion] ((wv : v.Extension L) → wv.1.Completion) :=
…
```
theorem NumberField.InfinitePlace.Completion.mem_placesOver_iff_comap line 108 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace, Iff, Membership.mem, Set, NumberField.InfinitePlace.placesOver, Eq, NumberField.InfinitePlace.comap, Algebra.algebraMap
Proof uses: id, Iff.intro, NumberField.InfinitePlace.LiesOver, NumberField.InfinitePlace.LiesOver.comap_eq, AbsoluteValue.LiesOver.mk, Real, AbsoluteValue, Exists, RingHom, Complex, NumberField.place, of_eq_true, AbsoluteValue.comp, FaithfulSMul.algebraMap_injective, Eq.trans, True, congrArg, Subtype.mk, Eq.symm, eq_self
18 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
instance NumberField.InfinitePlace.Completion.(instance at line 119) line 119 source
Source comment
A shortcut as this instance takes a while to synth
```
instance : Module.Free v.Completion wv.1.Completion :=
…
```
theorem NumberField.InfinitePlace.Completion.finrank_prod_eq_finrank line 125 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace, NumberField, Eq, Nat, Module.finrank, NumberField.InfinitePlace.Completion, NumberField.InfinitePlace.Extension, NumberField.InfinitePlace.comap, Algebra.algebraMap, NumberField.LiesOver.instAlgebraCompletion
Proof uses: Eq.mpr, Finset.sum, Finset.univ, Classical.propDecidable, id, congrArg, Module.finrank_pi_fintype, Set.toFinset, NumberField.InfinitePlace.placesOver, Membership.mem, Set, NumberField.InfinitePlace.inertiaDeg, Eq.symm, NumberField.InfinitePlace.sum_inertiaDeg_eq_finrank, Finset.sum_congr, rfl, Finset, NumberField.InfinitePlace.inertiaDeg_eq_finrank, Subtype, Finset.sum_subtype and 5 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem NumberField.InfinitePlace.Completion.finrank_pi_eq_finrank_tensorProduct line 133 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace, NumberField, Eq, Nat, Module.finrank, NumberField.InfinitePlace.Completion, NumberField.InfinitePlace.Extension, NumberField.InfinitePlace.comap, Algebra.algebraMap, NumberField.LiesOver.instAlgebraCompletion, TensorProduct, Real, AbsoluteValue, Exists, RingHom, Complex, NumberField.place, TensorProduct.RightActions.instModule_fLT
Proof uses: Eq.mpr, id, congrArg, TensorProduct.RightActions.instAlgebra_fLT, LinearEquiv.finrank_eq, AlgEquiv.symm, TensorProduct.RightActions.Algebra.TensorProduct.comm, HMul.hMul, Module.finrank_tensorProduct, OfNat.ofNat, Module.finrank_self, one_mul, NumberField.InfinitePlace.Completion.finrank_prod_eq_finrank, Eq.refl
93 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem NumberField.InfinitePlace.Completion.baseChange_surjective line 143 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace, NumberField, Function.Surjective, TensorProduct, NumberField.InfinitePlace.Completion, Real, AbsoluteValue, Exists, RingHom, Complex, Eq, NumberField.place, NumberField.InfinitePlace.Extension, NumberField.InfinitePlace.comap, Algebra.algebraMap, AlgHom, NumberField.InfinitePlace.Completion.baseChange
Proof uses: Module.Basis, Fin, Module.finrank, NumberField.LiesOver.instAlgebraCompletion, Module.finBasis, DenseRange, Subtype, NumberField.InfinitePlace.Completion.denseRange_algebraMap_subtype_pi, Ne, Matrix.det, Module.Basis.toMatrix, Pi.map, OfNat.ofNat, DenseRange.exists_matrix_det_ne_zero, Classical.propDecidable, Basis.toMatrix_continuous, NumberField.LiesOver.instContinuousSMulCompletion, DenseRange.piMap, Module.Basis.toMatrix_self, Eq.mpr and 45 more
145 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
theorem NumberField.InfinitePlace.Completion.baseChange_injective line 162 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace, NumberField, Function.Injective, TensorProduct, NumberField.InfinitePlace.Completion, Real, AbsoluteValue, Exists, RingHom, Complex, Eq, NumberField.place, NumberField.InfinitePlace.Extension, NumberField.InfinitePlace.comap, Algebra.algebraMap, AlgHom, NumberField.InfinitePlace.Completion.baseChange
Proof uses: Eq.mpr, TensorProduct.RightActions.instAlgebra_fLT, RingHom.toAlgebra, SemialgHom.toRingHom, NumberField.InfinitePlace.Completion.piExtension, SemialgHom.baseChangeRightOfAlgebraMap, id, congrArg, SemialgHom.baseChangeOfAlgebraMap, Eq.symm, SemialgHom.baseChangeRightOfAlgebraMap_coe, LinearMap, RingHom.id, AlgHom.toLinearMap, AlgHom.coe_toLinearMap, Function.Surjective, TensorProduct.RightActions.instModule_fLT, NumberField.LiesOver.instAlgebraCompletion, propext, LinearMap.injective_iff_surjective_of_finrank_eq_finrank and 9 more
75 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
instance NumberField.InfinitePlace.Completion.(instance at line 169) line 169 source
def NumberField.InfinitePlace.Completion.baseChangeEquiv The L-algebra homeomorphism between L ⊗[K] v.Completion and the product of all completions of L lying above v line 176 source
Source documentation
The L-algebra homeomorphism between L ⊗[K] v.Completion and the product of all completions of L lying above v.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace, NumberField, ContinuousAlgEquiv, TensorProduct, NumberField.InfinitePlace.Completion, Real, AbsoluteValue, Exists, RingHom, Complex, Eq, NumberField.place, NumberField.InfinitePlace.Extension, NumberField.InfinitePlace.comap, Algebra.algebraMap
Proof uses: AlgEquiv, AlgEquiv.ofBijective, NumberField.InfinitePlace.Completion.baseChange, IsBiscalar, TensorProduct.RightActions.instModule_fLT, NumberField.LiesOver.instAlgebraCompletion, AlgHom, IsModuleTopology.continuousAlgEquivOfIsBiscalar, TensorProduct.RightActions.instAlgebra_fLT
80 instances, coercions and auxiliary constants left out.
```
def baseChangeEquiv :
    L ⊗[K] v.Completion ≃A[L] (wv : v.Extension L) → wv.1.Completion :=
…
```
instance NumberField.InfinitePlace.Completion.(instance at line 184) line 184 source
theorem NumberField.InfinitePlace.Completion.baseChangeEquiv_tmul line 188 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace, NumberField, NumberField.InfinitePlace.Completion, Eq, NumberField.InfinitePlace.Extension, NumberField.InfinitePlace.comap, Algebra.algebraMap, ContinuousAlgEquiv, TensorProduct, Real, AbsoluteValue, Exists, RingHom, Complex, NumberField.place, NumberField.InfinitePlace.Completion.baseChangeEquiv, TensorProduct.tmul, HMul.hMul and 6 more
Proof uses: id, Eq.refl, AlgEquiv, AlgEquiv.ofBijective, SemialgHom.baseChangeOfAlgebraMap, NumberField.InfinitePlace.Completion.piExtension
91 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def NumberField.InfinitePlace.Completion.piEquiv The Kᵥ-linear homeomorphism between Kᵥ^d and the product of all completions of L lying above v, where d = [K : L] line 196 source
Source documentation
The Kᵥ-linear homeomorphism between Kᵥ^d and the product of all completions of L lying above v, where d = [K : L].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace, NumberField, ContinuousLinearEquiv, NumberField.InfinitePlace.Completion, RingHom.id, Fin, Module.finrank, NumberField.InfinitePlace.Extension, Eq, NumberField.InfinitePlace.comap, Algebra.algebraMap, NumberField.LiesOver.instAlgebraCompletion
Proof uses: LinearEquiv, TensorProduct, Real, AbsoluteValue, Exists, RingHom, Complex, NumberField.place, TensorProduct.RightActions.instAlgebra_fLT, AlgEquiv.symm, TensorProduct.RightActions.Algebra.TensorProduct.comm, TensorProduct.AlgebraTensorModule.finiteEquivPi, ContinuousLinearEquiv.symm, IsModuleTopology.continuousLinearEquiv, LinearEquiv.trans, ContinuousLinearEquiv.trans, ContinuousAlgEquiv.changeScalars, NumberField.InfinitePlace.Completion.baseChangeEquiv
79 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def piEquiv :
    (Fin (Module.finrank K L) → v.Completion) ≃L[v.Completion]
      (wv : v.Extension L) → wv.1.Completion := by
…
```
theorem NumberField.InfinitePlace.Completion.piEquiv_smul line 211 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfinitePlace, NumberField, NumberField.InfinitePlace.Completion, Fin, Module.finrank, NumberField.InfinitePlace.Extension, Eq, NumberField.InfinitePlace.comap, Algebra.algebraMap, ContinuousLinearEquiv, RingHom.id, NumberField.LiesOver.instAlgebraCompletion, NumberField.InfinitePlace.Completion.piEquiv, HSMul.hSMul, HMul.hMul, SemialgHom, Real, AbsoluteValue and 6 more
Proof uses: Eq.mpr, id, congrFun', congrArg, congrFun, ContinuousLinearEquiv.map_smul, NumberField.LiesOver.completionMap, Eq.refl
101 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.