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

27 declarations, 0 contain sorry, 0 declared as axioms

A result related to the Haar character of the finite adele ring of a number field

We prove the crucial result that left and right multiplication by an element of D ⊗[K] 𝔸_K^f scale Haar measure by the same factor, if D is a finite-dimensional central simple K-alegbra.

The proof looks simple on paper. We know the analogous result for finite-dimensional central simple algebras over local fields, but the proof essentially uses fields. I had thought that the adelic case would follow easily from this and from the fact that the haar character of a restricted product of maps was the product of the haar characters, but D ⊗[K] 𝔸_K^f is not a restricted product, and furthermore making it a restricted product is not completely formal because the compact open subrings 𝓞ᵥ used in the restricted product are not K-modules. One could either choose a lattice in D and work with that, or choose a basis of D and reduce first to to (𝔸_K^f)^n and then to Πʳ[Kᵥ^n,𝓞ᵥ^n], which is what we do.

Imports (17)

Imported by 2 files

def FiniteAdeleRing.Aux.f Documented declaration: f line 80 source
Source documentation
If φ : 𝔸_K^f ⊗[K] B ≃ 𝔸_K^f ⊗[K] B is continuous and 𝔸_K^f-linear then f φ is the associated continuous linear isomorphism (𝔸_K^f)^n ≃ (𝔸_K^f)^n coming from the "canonical" K-basis of B.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, FiniteDimensional, ContinuousLinearEquiv, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, RingHom.id, TensorProduct, Module.Free.ChooseBasisIndex
Proof uses: Module.Basis, Module.Free.chooseBasis, Module.Basis.baseChange, ContinuousLinearEquiv.trans, ContinuousLinearEquiv.symm, ContinuousLinearEquiv.chooseBasisPiScalarRight'
69 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
noncomputable def FiniteAdeleRing.Aux.f
    (φ : ((FiniteAdeleRing (𝓞 K) K) ⊗[K] B) ≃L[FiniteAdeleRing (𝓞 K) K]
      (FiniteAdeleRing (𝓞 K) K) ⊗[K] B) :
    (Module.Free.ChooseBasisIndex K B → (FiniteAdeleRing (𝓞 K) K)) ≃L[FiniteAdeleRing (𝓞 K) K]
    (Module.Free.ChooseBasisIndex K B → (FiniteAdeleRing (𝓞 K) K)) := by
…
```
lemma FiniteAdeleRing.Aux.f_commSq line 92 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, FiniteDimensional, ContinuousLinearEquiv, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, RingHom.id, TensorProduct, Eq, NNReal, MeasureTheory.addEquivAddHaarChar, ContinuousLinearEquiv.toContinuousAddEquiv, Module.Free.ChooseBasisIndex, FiniteAdeleRing.Aux.f
Proof uses: MeasureTheory.addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv, ContinuousLinearEquiv.chooseBasisPiScalarRight', id, ContinuousAddEquiv, of_eq_true, ContinuousLinearEquiv.symm, Eq.trans, True, congrArg, ContinuousLinearEquiv.symm_apply_apply, eq_self
142 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
def FiniteAdeleRing.Aux.g If ψ : (𝔸_K^f)^n ≃ (𝔸_K^f)^n is continuous and 𝔸_K^f-linear then g φ is the associated continuous additive isomorphism Πʳ[Kᵥ^n, 𝓞ᵥ^n] → Πʳ[Kᵥ^n,𝓞ᵥ^n] line 160 source
Source documentation
If ψ : (𝔸_K^f)^n ≃ (𝔸_K^f)^n is continuous and 𝔸_K^f-linear then g φ is the associated continuous additive isomorphism Πʳ[Kᵥ^n, 𝓞ᵥ^n] → Πʳ[Kᵥ^n,𝓞ᵥ^n].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Fintype, ContinuousLinearEquiv, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, RingHom.id, ContinuousAddEquiv, RestrictedProduct, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.adicCompletion, AddSubgroup, AddSubgroup.pi, Set.univ, Subring.toAddSubgroup, ValuationSubring.toSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Filter.cofinite
Proof uses: ContinuousAddEquiv.trans, ContinuousAddEquiv.restrictedProductPi, NumberField.isOpenAdicCompletionIntegers, ContinuousLinearEquiv.toContinuousAddEquiv, ContinuousAddEquiv.symm
90 instances, coercions and auxiliary constants left out.
```
noncomputable def FiniteAdeleRing.Aux.g {ι : Type*} [Fintype ι]
    (ψ : (ι → (FiniteAdeleRing (𝓞 K) K)) ≃L[FiniteAdeleRing (𝓞 K) K]
      (ι → (FiniteAdeleRing (𝓞 K) K))) :
    Πʳ (v : HeightOneSpectrum (𝓞 K)), [ι → v.adicCompletion K,
      (AddSubgroup.pi (Set.univ : Set ι) (fun _ ↦ (v.adicCompletionIntegers K).toAddSubgroup))] ≃ₜ+
    Πʳ (v : HeightOneSpectrum (𝓞 K)), [ι → v.adicCompletion K,
      (AddSubgroup.pi (Set.univ : Set ι) (fun _ ↦ (v.adicCompletionIntegers K).toAddSubgroup))] :=
…
```
lemma FiniteAdeleRing.Aux.g_commSq line 173 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Fintype, ContinuousLinearEquiv, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, RingHom.id, Eq, NNReal, MeasureTheory.addEquivAddHaarChar, ContinuousLinearEquiv.toContinuousAddEquiv, RestrictedProduct, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.adicCompletion, AddSubgroup, AddSubgroup.pi, Set.univ, Subring.toAddSubgroup, ValuationSubring.toSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers and 5 more
Proof uses: Eq.symm, ContinuousAddEquiv, ContinuousAddEquiv.restrictedProductPi, NumberField.isOpenAdicCompletionIntegers, MeasureTheory.addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv, id, of_eq_true, ContinuousAddEquiv.symm, Subring, Eq.trans, True, congrFun', congrArg, ContinuousAddEquiv.apply_symm_apply, eq_self
161 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
def FiniteAdeleRing.Aux.e If φ : Kᵥ ⊗[K] B ≃ Kᵥ ⊗[K] B is continuous and additive then f φ is the associated continuous additive isomorphism Kᵥ^n ≃ Kᵥ^n coming from the "canonical" K-basis of B line 210 source
Source documentation
If φ : Kᵥ ⊗[K] B ≃ Kᵥ ⊗[K] B is continuous and additive then f φ is the associated continuous additive isomorphism Kᵥ^n ≃ Kᵥ^n coming from the "canonical" K-basis of B.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, FiniteDimensional, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, ContinuousLinearEquiv, RingHom.id, TensorProduct, IsDedekindDomain.HeightOneSpectrum.adicCompletion, ContinuousAddEquiv, Module.Free.ChooseBasisIndex
Proof uses: Module.Basis, Module.Free.chooseBasis, Module.Basis.baseChange, ContinuousLinearEquiv.toContinuousAddEquiv, ContinuousLinearEquiv.chooseBasisPiScalarRight', ContinuousAddEquiv.trans, ContinuousAddEquiv.symm
77 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
noncomputable def FiniteAdeleRing.Aux.e (v : HeightOneSpectrum (𝓞 K))
    (α : v.adicCompletion K ⊗[K] B ≃L[K] v.adicCompletion K ⊗[K] B) :
    (Module.Free.ChooseBasisIndex K B → (v.adicCompletion K)) ≃ₜ+
    (Module.Free.ChooseBasisIndex K B → (v.adicCompletion K)) := by
…
```
lemma FiniteAdeleRing.Aux.e_commSq line 233 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, FiniteDimensional, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, ContinuousLinearEquiv, RingHom.id, TensorProduct, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Eq, NNReal, MeasureTheory.addEquivAddHaarChar, ContinuousLinearEquiv.toContinuousAddEquiv, Module.Free.ChooseBasisIndex, WithZero, Multiplicative, Int, FiniteAdeleRing.Aux.e
Proof uses: MeasureTheory.addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv, ContinuousLinearEquiv.chooseBasisPiScalarRight', id, ContinuousAddEquiv, of_eq_true, ContinuousLinearEquiv.symm, Eq.trans, True, congrArg, ContinuousLinearEquiv.symm_apply_apply, eq_self
181 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
abbrev bLocal bLocal is v.adicCompletion K-basis for v.adicCompletion K ⊗[K] B line 257 source
Source documentation
bLocal is v.adicCompletion K-basis for v.adicCompletion K ⊗[K] B.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, FiniteDimensional, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Module.Basis, Module.Free.ChooseBasisIndex, IsDedekindDomain.HeightOneSpectrum.adicCompletion, TensorProduct
Proof uses: Module.Basis.baseChange, Module.Free.chooseBasis
44 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev bLocal (v : HeightOneSpectrum (𝓞 K)) :=
…
```
abbrev bGlobal bGlobal is FiniteAdeleRing (𝓞 K) K-basis for FiniteAdeleRing (𝓞 K) K ⊗[K] B line 261 source
Source documentation
bGlobal is FiniteAdeleRing (𝓞 K) K-basis for FiniteAdeleRing (𝓞 K) K ⊗[K] B.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, FiniteDimensional, Module.Basis, Module.Free.ChooseBasisIndex, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, TensorProduct
Proof uses: Module.Basis.baseChange, Module.Free.chooseBasis
44 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev bGlobal :=
…
```
lemma basis_repr_eq line 264 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, FiniteDimensional, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, TensorProduct, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Eq, Module.Free.ChooseBasisIndex, Finsupp, LinearEquiv, RingHom.id, Module.Basis.repr, bLocal, ContinuousLinearEquiv, ContinuousLinearEquiv.chooseBasisPiScalarRight'
Proof uses: TensorProduct.inductionOn, funext, TensorProduct.tmul, IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext, Eq.mpr, Valuation.Completion, WithZero, Multiplicative, Int, IsDedekindDomain.HeightOneSpectrum.valuation, IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion, HSMul.hSMul, Module.Free.chooseBasis, id, congrFun', congrArg, Module.Basis.baseChange_repr_tmul, Eq.refl, of_eq_true, HAdd.hAdd and 7 more
141 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma basis_repr_eq_global line 270 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, FiniteDimensional, TensorProduct, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Eq, Module.Free.ChooseBasisIndex, Finsupp, LinearEquiv, RingHom.id, Module.Basis.repr, bGlobal, ContinuousLinearEquiv, ContinuousLinearEquiv.chooseBasisPiScalarRight'
Proof uses: TensorProduct.inductionOn, funext, TensorProduct.tmul, IsDedekindDomain.FiniteAdeleRing.ext, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Eq.mpr, Valuation.Completion, WithZero, Multiplicative, Int, IsDedekindDomain.HeightOneSpectrum.valuation, IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion, HSMul.hSMul, Module.Free.chooseBasis, id, congrFun', congrArg, congrFun and 11 more
140 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma basis_eq_single line 276 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, FiniteDimensional, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Module.Free.ChooseBasisIndex, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Eq, TensorProduct, HSMul.hSMul, Module.Basis, bLocal, ContinuousLinearEquiv, RingHom.id, ContinuousLinearEquiv.symm, ContinuousLinearEquiv.chooseBasisPiScalarRight', Pi.single
Proof uses: Eq.mpr, id, congrArg, propext, ContinuousLinearEquiv.eq_symm_apply, funext, TensorProduct.tmul, Module.Free.chooseBasis, of_eq_true, Eq.trans, True, congrFun', HMul.hMul, RingHom, Algebra.algebraMap, OfNat.ofNat, Module.Basis.baseChange_apply, Algebra.smul_def, congr, mul_one and 31 more
167 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma basis_eq line 290 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, FiniteDimensional, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Module.Free.ChooseBasisIndex, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Eq, TensorProduct, Finset.sum, Finset.univ, HSMul.hSMul, Module.Basis, bLocal, ContinuousAddEquiv, ContinuousAddEquiv.symm, ContinuousLinearEquiv.toContinuousAddEquiv, ContinuousLinearEquiv.chooseBasisPiScalarRight'
Proof uses: Pi.single, funext, IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext, of_eq_true, Valuation.Completion, WithZero, Multiplicative, Int, IsDedekindDomain.HeightOneSpectrum.valuation, IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion, Eq.trans, True, congrArg, Finset.sum_apply, ite, Membership.mem, Finset, OfNat.ofNat, Finset.sum_pi_single, ite_eq_left_of_eq_true and 12 more
145 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma basis_eq_single_global line 300 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, FiniteDimensional, Module.Free.ChooseBasisIndex, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Eq, TensorProduct, HSMul.hSMul, Module.Basis, bGlobal, ContinuousLinearEquiv, RingHom.id, ContinuousLinearEquiv.symm, ContinuousLinearEquiv.chooseBasisPiScalarRight', Pi.single
Proof uses: Eq.mpr, id, congrArg, propext, ContinuousLinearEquiv.eq_symm_apply, funext, IsDedekindDomain.FiniteAdeleRing.ext, IsDedekindDomain.HeightOneSpectrum, TensorProduct.tmul, Module.Free.chooseBasis, of_eq_true, Eq.trans, True, congrFun', HMul.hMul, RingHom, Algebra.algebraMap, OfNat.ofNat, Module.Basis.baseChange_apply, Algebra.smul_def and 35 more
160 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma basis_eq_global line 314 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, FiniteDimensional, Module.Free.ChooseBasisIndex, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Eq, TensorProduct, Finset.sum, Finset.univ, HSMul.hSMul, Module.Basis, bGlobal, ContinuousAddEquiv, ContinuousAddEquiv.symm, ContinuousLinearEquiv.toContinuousAddEquiv, ContinuousLinearEquiv.chooseBasisPiScalarRight'
Proof uses: Pi.single, funext, IsDedekindDomain.FiniteAdeleRing.ext, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext, IsDedekindDomain.HeightOneSpectrum.adicCompletion, of_eq_true, Valuation.Completion, WithZero, Multiplicative, Int, IsDedekindDomain.HeightOneSpectrum.valuation, IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion, Eq.trans, True, congrArg, congrFun, Finset.sum_apply, ite, Membership.mem and 16 more
142 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def φLocalKvLinear TensorProduct.localcomponent φ as v.adicCompletion K-linear map line 329 source
Source documentation
TensorProduct.localcomponent φ as v.adicCompletion K-linear map

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, FiniteDimensional, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, ContinuousLinearEquiv, IsDedekindDomain.FiniteAdeleRing, RingHom.id, TensorProduct, LinearMap, IsDedekindDomain.HeightOneSpectrum.adicCompletion
Proof uses: IsDedekindDomain.FiniteAdeleRing.TensorProduct.localcomponentEquiv, LinearMap.mk, LinearMap.toAddHom
65 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
noncomputable def φLocalKvLinear (v : HeightOneSpectrum (𝓞 K))
    (φ : FiniteAdeleRing (𝓞 K) K ⊗[K] B ≃L[FiniteAdeleRing (𝓞 K) K]
    FiniteAdeleRing (𝓞 K) K ⊗[K] B) :
    v.adicCompletion K ⊗[K] B →ₗ[v.adicCompletion K] v.adicCompletion K ⊗[K] B := {
…
```
lemma localcomponent_matrix line 361 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, FiniteDimensional, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, ContinuousLinearEquiv, IsDedekindDomain.FiniteAdeleRing, RingHom.id, TensorProduct, Module.Free.ChooseBasisIndex, Eq, IsDedekindDomain.HeightOneSpectrum.adicCompletion, LinearEquiv, LinearMap, Matrix, LinearMap.toMatrix, Module.Basis.baseChange, Module.Free.chooseBasis and 1 more
Proof uses: Module.Basis, id, congr_fun, RingHom, RestrictedProduct, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Filter.cofinite, RingHom.mapMatrix, RestrictedProduct.evalRingHom, Eq.mpr, Matrix.map, congrArg, RingHom.mapMatrix_apply, LinearEquiv.injective, Matrix.toLin, Matrix.toLin_toMatrix, TensorProduct.AlgebraTensorModule.curry_injective, LinearMap.ext_ring, TensorProduct.AlgebraTensorModule.curry and 63 more
190 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
lemma toMatrix_f The matrix reps of φ and f φ agree line 449 source
Source documentation
The matrix reps of φ and f φ agree.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, FiniteDimensional, ContinuousLinearEquiv, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, RingHom.id, TensorProduct, Eq, Matrix, Module.Free.ChooseBasisIndex, LinearEquiv, LinearMap, LinearMap.toMatrix, bGlobal, LinearMap.toMatrix', FiniteAdeleRing.Aux.f
Proof uses: Finset.sum, Finset.univ, HSMul.hSMul, Module.Basis, ContinuousLinearEquiv.symm, ContinuousLinearEquiv.chooseBasisPiScalarRight', basis_eq_global, Matrix.ext, IsDedekindDomain.FiniteAdeleRing.ext, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext, IsDedekindDomain.HeightOneSpectrum.adicCompletion, of_eq_true, Valuation.Completion, WithZero, Multiplicative, Int, IsDedekindDomain.HeightOneSpectrum.valuation, IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion, Eq.trans and 28 more
166 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma toMatrix_f
    (φ : FiniteAdeleRing (𝓞 K) K ⊗[K] B ≃L[FiniteAdeleRing (𝓞 K) K]
      FiniteAdeleRing (𝓞 K) K ⊗[K] B) :
    LinearMap.toMatrix (bGlobal K B) (bGlobal K B) φ.toLinearEquiv
    = LinearMap.toMatrix' (f K B φ) := by
…
```
Mentions: bGlobal
lemma FiniteAdeleRing.Aux.almost_always_mapsTo A (continuous) 𝔸_K^f-linear automorphism of 𝔸_K^f ⊗ B is "integral" at all but finitely many places line 466 source
Source comment
A (continuous) 𝔸_K^f-linear automorphism of 𝔸_K^f ⊗ B is "integral" at all but finitely many places

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, FiniteDimensional, ContinuousLinearEquiv, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, RingHom.id, TensorProduct, Filter.Eventually, IsDedekindDomain.HeightOneSpectrum, Set.MapsTo, Module.Free.ChooseBasisIndex, IsDedekindDomain.HeightOneSpectrum.adicCompletion, ContinuousAddEquiv, FiniteAdeleRing.Aux.e, IsDedekindDomain.FiniteAdeleRing.TensorProduct.localcomponentEquiv, AddSubgroup, AddSubgroup.pi and 5 more
Proof uses: Module.Basis, Module.Free.chooseBasis, Module.Basis.baseChange, Matrix, LinearEquiv, LinearMap, LinearMap.toMatrix, Membership.mem, Set, ValuationSubring, Subtype.property, Filter.mp_mem, Set.ofPred, Eq.mp, Eq.trans, forall_congr, Filter.univ_mem', id, Eq, Finsupp and 38 more
218 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma FiniteAdeleRing.Aux.almost_always_mapsTo
    (φ : FiniteAdeleRing (𝓞 K) K ⊗[K] B ≃L[FiniteAdeleRing (𝓞 K) K]
    FiniteAdeleRing (𝓞 K) K ⊗[K] B) :
    letI ι := Module.Free.ChooseBasisIndex K B
…
```
lemma FiniteAdeleRing.Aux.almost_always_bijOn A (continuous) 𝔸_K^f-linear automorphism of 𝔸_K^f ⊗ B is "integral" at all but finitely many places line 507 source
Source comment
A (continuous) 𝔸_K^f-linear automorphism of 𝔸_K^f ⊗ B is "integral" at all but finitely many places

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, FiniteDimensional, ContinuousLinearEquiv, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, RingHom.id, TensorProduct, Filter.Eventually, IsDedekindDomain.HeightOneSpectrum, Set.BijOn, Module.Free.ChooseBasisIndex, IsDedekindDomain.HeightOneSpectrum.adicCompletion, ContinuousAddEquiv, FiniteAdeleRing.Aux.e, IsDedekindDomain.FiniteAdeleRing.TensorProduct.localcomponentEquiv, AddSubgroup, AddSubgroup.pi and 5 more
Proof uses: Set.MapsTo, FiniteAdeleRing.Aux.almost_always_mapsTo, ContinuousLinearEquiv.symm, Filter.mp_mem, Set.ofPred, Membership.mem, Set, Filter.univ_mem', id, Equiv.bijOn', AddEquiv.toEquiv, ContinuousAddEquiv.toAddEquiv
133 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma FiniteAdeleRing.Aux.almost_always_bijOn
    (φ : FiniteAdeleRing (𝓞 K) K ⊗[K] B ≃L[FiniteAdeleRing (𝓞 K) K]
    FiniteAdeleRing (𝓞 K) K ⊗[K] B) :
    letI ι := Module.Free.ChooseBasisIndex K B
…
```
lemma FiniteAdeleRing.Aux.f_g_local_global A diagram which obviously commutes, commutes line 524 source
Source documentation
A diagram which obviously commutes, commutes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, FiniteDimensional, ContinuousLinearEquiv, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, RingHom.id, TensorProduct, Eq, ContinuousAddEquiv, RestrictedProduct, IsDedekindDomain.HeightOneSpectrum, Module.Free.ChooseBasisIndex, IsDedekindDomain.HeightOneSpectrum.adicCompletion, AddSubgroup, AddSubgroup.pi, Set.univ, Subring.toAddSubgroup and 9 more
Proof uses: ContinuousAddEquiv.ext, RestrictedProduct.ext, funext, Module.Basis, Module.Free.chooseBasis, Module.Basis.baseChange, Matrix, LinearEquiv, LinearMap, LinearMap.toMatrix, id, Eq.mpr, ContinuousAddEquiv.trans, ContinuousAddEquiv.symm, ContinuousLinearEquiv.toContinuousAddEquiv, ContinuousLinearEquiv.chooseBasisPiScalarRight', RestrictedProduct.map, AddEquiv, AddEquiv.toEquiv, ContinuousAddEquiv.toAddEquiv and 66 more
278 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma FiniteAdeleRing.Aux.f_g_local_global
    (φ : ((FiniteAdeleRing (𝓞 K) K) ⊗[K] B) ≃L[FiniteAdeleRing (𝓞 K) K]
      (FiniteAdeleRing (𝓞 K) K) ⊗[K] B) :
    g K (f K B φ) = ContinuousAddEquiv.restrictedProductCongrRight
    (fun v ↦ e _ _ _ (FiniteAdeleRing.TensorProduct.localcomponentEquiv (𝓞 K) K B v φ))
    (FiniteAdeleRing.Aux.almost_always_bijOn _ _ _) := by
…
```
Mentions: FiniteAdeleRing.Aux.g, FiniteAdeleRing.Aux.f, FiniteAdeleRing.Aux.e, FiniteAdeleRing.Aux.almost_always_bijOn
lemma localcomponent_mulLeft line 568 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, FiniteDimensional, Units, TensorProduct, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, IsDedekindDomain.HeightOneSpectrum, Eq, ContinuousAddEquiv, IsDedekindDomain.HeightOneSpectrum.adicCompletion, ContinuousLinearEquiv.toContinuousAddEquiv, IsDedekindDomain.FiniteAdeleRing.TensorProduct.localcomponentEquiv, ContinuousLinearEquiv.mulLeft, ContinuousAddEquiv.mulLeft, MonoidHom, Units.map, AlgHom.toRingHom and 2 more
Proof uses: ContinuousAddEquiv.ext, ContinuousLinearMap, RingHom.id, ContinuousLinearMap.rTensor', WithZero, Multiplicative, Int, ContinuousAlgHom.toContinuousLinearMap, LinearMap, TensorProduct.map, IsDedekindDomain.FiniteAdeleRing.singleContinuousLinearMap, LinearMap.id, IsDedekindDomain.FiniteAdeleRing.TensorProduct.localcomponent, IsDedekindDomain.FiniteAdeleRing.TensorProduct.localcomponent_apply, LinearMap.comp, LinearMap.ext, IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext, of_eq_true, Valuation.Completion, IsDedekindDomain.HeightOneSpectrum.valuation and 29 more
196 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma localcomponent_mulRight line 593 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, FiniteDimensional, Units, TensorProduct, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, IsDedekindDomain.HeightOneSpectrum, Eq, ContinuousAddEquiv, IsDedekindDomain.HeightOneSpectrum.adicCompletion, ContinuousLinearEquiv.toContinuousAddEquiv, IsDedekindDomain.FiniteAdeleRing.TensorProduct.localcomponentEquiv, ContinuousLinearEquiv.mulRight, ContinuousAddEquiv.mulRight, MonoidHom, Units.map, AlgHom.toRingHom and 2 more
Proof uses: ContinuousAddEquiv.ext, ContinuousLinearMap, RingHom.id, ContinuousLinearMap.rTensor', WithZero, Multiplicative, Int, ContinuousAlgHom.toContinuousLinearMap, LinearMap, TensorProduct.map, IsDedekindDomain.FiniteAdeleRing.singleContinuousLinearMap, LinearMap.id, IsDedekindDomain.FiniteAdeleRing.TensorProduct.localcomponent, IsDedekindDomain.FiniteAdeleRing.TensorProduct.localcomponent_apply, LinearMap.comp, LinearMap.ext, IsDedekindDomain.HeightOneSpectrum.adicCompletion.ext, of_eq_true, Valuation.Completion, IsDedekindDomain.HeightOneSpectrum.valuation and 29 more
196 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma NumberField.FiniteAdeleRing.tensor_isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul left multiplication and right multiplication by a unit have the same Haar character on 𝔸_K^f ⊗ B line 623 source
Source documentation
left multiplication and right multiplication by a unit have the same Haar character on 𝔸_K^f ⊗ B. See also NumberField.FiniteAdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul which proves it for B ⊗ 𝔸_K^f.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, FiniteDimensional, IsSimpleRing, Algebra.IsCentral, Units, TensorProduct, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Eq, NNReal, MeasureTheory.addEquivAddHaarChar, ContinuousAddEquiv.mulLeft, ContinuousAddEquiv.mulRight
Proof uses: id, Eq.mpr, ContinuousLinearEquiv.toContinuousAddEquiv, ContinuousLinearEquiv.mulLeft, ContinuousLinearEquiv.mulRight, Module.Free.ChooseBasisIndex, FiniteAdeleRing.Aux.f, congrArg, FiniteAdeleRing.Aux.f_commSq, RestrictedProduct, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.adicCompletion, AddSubgroup, AddSubgroup.pi, Set.univ, Subring.toAddSubgroup, ValuationSubring.toSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Filter.cofinite, WithZero and 28 more
210 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma NumberField.FiniteAdeleRing.tensor_isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul
    [IsSimpleRing B] [Algebra.IsCentral K B] (u : ((FiniteAdeleRing (𝓞 K) K) ⊗[K] B)ˣ) :
    addEquivAddHaarChar (ContinuousAddEquiv.mulLeft u) =
    addEquivAddHaarChar (ContinuousAddEquiv.mulRight u) := by
…
```
instance (instance at line 651) line 651 source
def FiniteAdeleRing.TensorProduct.commLinearMap B ⊗ 𝔸_K^f ≃ 𝔸_K^f ⊗ B as 𝔸_K^f-modules line 661 source
Source documentation
B ⊗ 𝔸_K^f ≃ 𝔸_K^f ⊗ B as 𝔸_K^f-modules.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, LinearEquiv, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, RingHom.id, TensorProduct, TensorProduct.RightActions.instModule_fLT
Proof uses: TensorProduct.comm, LinearEquiv.mk, LinearMap.mk, LinearMap.toAddHom, LinearEquiv.invFun
44 instances, coercions and auxiliary constants left out.
```
noncomputable def FiniteAdeleRing.TensorProduct.commLinearMap :
    (B ⊗[K] (FiniteAdeleRing (𝓞 K) K)) ≃ₗ[FiniteAdeleRing (𝓞 K) K]
    (FiniteAdeleRing (𝓞 K) K) ⊗[K] B := {
…
```
def FiniteAdeleRing.TensorProduct.commContinuousAddMonoidHom B ⊗ 𝔸_K^f ≃ 𝔸_K^f ⊗ B as topological additive groups line 670 source
Source documentation
B ⊗ 𝔸_K^f ≃ 𝔸_K^f ⊗ B as topological additive groups.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, FiniteDimensional, ContinuousAddEquiv, TensorProduct, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT
Proof uses: LinearEquiv, RingHom.id, TensorProduct.RightActions.instModule_fLT, FiniteAdeleRing.TensorProduct.commLinearMap, ContinuousAddEquiv.mk, AddEquiv.mk, Equiv.mk, AddHom.toFun, LinearMap.toAddHom, LinearEquiv.invFun
51 instances, coercions and auxiliary constants left out.
```
noncomputable def FiniteAdeleRing.TensorProduct.commContinuousAddMonoidHom :
    (B ⊗[K] (FiniteAdeleRing (𝓞 K) K)) ≃ₜ+
    (FiniteAdeleRing (𝓞 K) K) ⊗[K] B := {
…
```
lemma NumberField.FiniteAdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul left multiplication and right multiplication by a unit have the same Haar character on B ⊗ 𝔸_K^f line 689 source
Source documentation
left multiplication and right multiplication by a unit have the same Haar character on B ⊗ 𝔸_K^f. See also NumberField.FiniteAdeleRing.tensor_isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul which proves it for 𝔸_K^f ⊗ B.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, FiniteDimensional, MeasurableSpace, TensorProduct, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, BorelSpace, TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT, IsSimpleRing, Algebra.IsCentral, Units, Eq, NNReal, MeasureTheory.addEquivAddHaarChar, TensorProduct.RightActions.instIsTopologicalAddGroup_fLT, TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT, ContinuousAddEquiv.mulLeft and 2 more
Proof uses: MonoidHom, Units.map, AlgEquiv, Algebra.TensorProduct.comm, MeasureTheory.addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv, FiniteAdeleRing.TensorProduct.commContinuousAddMonoidHom, map_mul, MonoidHom.id, Eq.mpr, id, congrArg, NumberField.FiniteAdeleRing.tensor_isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul
100 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma NumberField.FiniteAdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul
    [IsSimpleRing B] [Algebra.IsCentral K B] (u : (B ⊗[K] (FiniteAdeleRing (𝓞 K) K))ˣ) :
    addEquivAddHaarChar (ContinuousAddEquiv.mulLeft u) =
    addEquivAddHaarChar (ContinuousAddEquiv.mulRight u) := by
…
```