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

52 declarations, 0 contain sorry, 0 declared as axioms

The adele ring of a number field

Defining base change

One of the main results in this file is base change, which is the L-algebra homeomorphism L ⊗[K] 𝔸_K ≃A[L] 𝔸_L for number fields L / K. Per the discussion in FLT.NumberField.InfiniteAdeleRing there are two approaches to defining this map (1) Piece together the base changes for the infinite and finite adele rings. (2) Follow the same path as that of the infinite and finite adele ring by lifing the map 𝔸 K → 𝔸 L

Previously both definitions were provided. Both still exist, but the first approach is the only one that is now used. The second approach is given at the end of the file and we show that both maps agree.

Bi-scalarity

The fact that L ⊗[K] 𝔸_K ≃A[L] 𝔸_L is both an L and an 𝔸 K algebra isomorphism is used heavily in this file, mainly because the topologies are 𝔸 K-module topologies. This property has been abstracted to a typeclass IsBiscalar defined in FLT.Mathlib.Algebra.Algebra.Tower. TODO: would it be better do define this as a bundled map →ₐ[L, 𝔸 K] rather than use a typeclass?

Diamonds

Diamonds of the form Algebra K L → Algebra (𝔸 K) (𝔸 L) have caused issues in the past, with instance search timing out when K = L. In FLT.NumberField.InfiniteAdeleRing we avoided this by adding [Algebra K∞ L∞] as assumptions alongside compatibility instances. A similar approach is taken here, with Prod.IsProdSMul being the only extra piece of compatibility required.

The desired instances are constructed later as scoped instances in FLT.NumberField.AdeleRing.

Imports (18)

Imported by 2 files

instance NumberField.AdeleRing.(instance at line 80) line 80 source
lemma NumberField.AdeleRing.smul_fst line 84 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, SMul, NumberField.InfiniteAdeleRing, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, NumberField.AdeleRing, Prod.IsProdSMul, Eq, Prod.fst, HSMul.hSMul
Proof uses: Eq.mpr, id, congrArg, Prod, Prod.IsProdSMul.smul_fst, Eq.refl
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma NumberField.AdeleRing.smul_snd line 91 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, SMul, NumberField.InfiniteAdeleRing, Algebra, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, NumberField.AdeleRing, Prod.IsProdSMul, Eq, Prod.snd, HSMul.hSMul
Proof uses: Eq.mpr, id, congrArg, Prod, Prod.IsProdSMul.smul_snd, Eq.refl
20 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def NumberField.AdeleRing.baseChange The canonical map from the adeles of K to the adeles of L line 100 source
Source documentation
The canonical map from the adeles of K to the adeles of L

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Algebra, ContinuousSemialgHom, Algebra.algebraMap, NumberField.AdeleRing, NumberField.RingOfIntegers
Proof uses: ContinuousSemialgHom.prodMap, NumberField.InfiniteAdeleRing, IsDedekindDomain.FiniteAdeleRing, NumberField.InfiniteAdeleRing.baseChange, IsDedekindDomain.FiniteAdeleRing.mapSemialgHom
32 instances, coercions and auxiliary constants left out.
```
noncomputable def baseChange :
    (𝔸 K) →SA[algebraMap K L] 𝔸 L :=
…
```
lemma NumberField.AdeleRing.baseChange_fst_apply line 104 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Algebra, NumberField.AdeleRing, NumberField.RingOfIntegers, Eq, NumberField.InfiniteAdeleRing, Prod.fst, IsDedekindDomain.FiniteAdeleRing, ContinuousSemialgHom, Algebra.algebraMap, NumberField.AdeleRing.baseChange, NumberField.InfiniteAdeleRing.baseChange
Proof uses: rfl
29 instances, coercions and auxiliary constants left out.
lemma NumberField.AdeleRing.baseChange_snd_apply line 106 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Algebra, NumberField.AdeleRing, NumberField.RingOfIntegers, Eq, IsDedekindDomain.FiniteAdeleRing, Prod.snd, NumberField.InfiniteAdeleRing, ContinuousSemialgHom, Algebra.algebraMap, NumberField.AdeleRing.baseChange, IsDedekindDomain.FiniteAdeleRing.mapSemialgHom
Proof uses: rfl
39 instances, coercions and auxiliary constants left out.
instance NumberField.AdeleRing.instPiIsModuleTopology line 111 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Algebra, IsModuleTopology, NumberField.AdeleRing, NumberField.RingOfIntegers, Fin, Module.finrank
41 instances, coercions and auxiliary constants left out.
def NumberField.AdeleRing.baseChangeAlgEquiv The L-algebra isomorphism L ⊗[K] 𝔸_K = 𝔸_L line 117 source
Source documentation
The L-algebra isomorphism L ⊗[K] 𝔸_K = 𝔸_L.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Algebra, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul, AlgEquiv, TensorProduct, NumberField.AdeleRing
Proof uses: Prod, NumberField.InfiniteAdeleRing, Algebra.TensorProduct.prodRight, AlgEquiv.prodCongr, NumberField.InfiniteAdeleRing.baseChangeAlgEquiv, IsDedekindDomain.FiniteAdeleRing.baseChangeAlgEquiv, AlgEquiv.trans
59 instances, coercions and auxiliary constants left out.
```
noncomputable def baseChangeAlgEquiv : (L ⊗[K] 𝔸 K) ≃ₐ[L] 𝔸 L :=
…
```
lemma NumberField.AdeleRing.baseChangeAlgEquiv_apply line 125 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Algebra, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul, NumberField.AdeleRing, Eq, AlgEquiv, TensorProduct, NumberField.AdeleRing.baseChangeAlgEquiv, TensorProduct.tmul, HMul.hMul, RingHom, Algebra.algebraMap, ContinuousSemialgHom, NumberField.AdeleRing.baseChange
Proof uses: Eq.refl
61 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma NumberField.AdeleRing.baseChangeAlgEquiv_fst_apply line 129 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Algebra, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul, NumberField.AdeleRing, Eq, NumberField.InfiniteAdeleRing, Prod.fst, AlgEquiv, TensorProduct, NumberField.AdeleRing.baseChangeAlgEquiv, TensorProduct.tmul, NumberField.InfiniteAdeleRing.baseChangeAlgEquiv
Proof uses: rfl
56 instances, coercions and auxiliary constants left out.
lemma NumberField.AdeleRing.baseChangeAlgEquiv_snd_apply line 133 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Algebra, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul, NumberField.AdeleRing, Eq, Prod.snd, NumberField.InfiniteAdeleRing, AlgEquiv, TensorProduct, NumberField.AdeleRing.baseChangeAlgEquiv, TensorProduct.tmul, IsDedekindDomain.FiniteAdeleRing.baseChangeAlgEquiv
Proof uses: rfl
56 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
instance NumberField.AdeleRing.(instance at line 153) line 153 source
Source documentation
Take arbitrary Algebra K L∞, Algebra K∞ L∞, Algebra 𝔸ᶠ[K] 𝔸ᶠ[L], Algebra K 𝔸ᶠ[L], Algebra (𝓞 K) 𝔸ᶠ[L]andAlgebra (𝔸 K) (𝔸 L)` instances. Assume:
- Algebra K L∞ factors through (existing) Algebra K L and Algebra L L∞.
- Algebra K∞ L∞ and Algebra 𝔸ᶠ[K] 𝔸ᶠ[L] are determined by the fibers of restriction of places of L to K via (x • y) v = x (v.comap (algebraMap K L)) • y v.
- Algebra K 𝔸ᶠ[L] factors through (existing) Algebra K L and Algebra L 𝔸ᶠ[L].
- Algebra (𝓞 K) 𝔸ᶠ[L] factors through Algebra (𝓞 K) (𝓞 L) and Algebra (𝓞 L) 𝔸ᶠ[L].
- Algebra (𝔸 K) (𝔸 L) is constructed as the product algebra from Algebra K∞ L∞ and Algebra 𝔸ᶠ[K] 𝔸ᶠ[L]. Then the Lalgebra base change map is also linear in𝔸 K`.
```
instance [Algebra K∞ L∞] [Algebra (𝔸 K) (𝔸 L)]
    [Pi.FiberwiseSMul (fun a => a.comap (algebraMap K L)) Completion Completion]
    [Prod.IsProdSMul K∞ 𝔸ᶠ[K] L∞ 𝔸ᶠ[L]] :
    IsBiscalar L (𝔸 K) (baseChangeAlgEquiv K L).toAlgHom where
…
```
Mentions: Pi.FiberwiseSMul, Prod.IsProdSMul, IsBiscalar, NumberField.AdeleRing.baseChangeAlgEquiv
def NumberField.AdeleRing.baseChangeEquiv The L-algebra homeomorphism L ⊗[K] 𝔸 K = 𝔸 L line 188 source
Source documentation
The L-algebra homeomorphism L ⊗[K] 𝔸 K = 𝔸 L.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Algebra, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul, NumberField.InfiniteAdeleRing, Pi.FiberwiseSMul, NumberField.InfinitePlace, NumberField.InfinitePlace.comap, Algebra.algebraMap, NumberField.InfinitePlace.Completion, Subtype, Eq, NumberField.LiesOver.instAlgebraCompletion, NumberField.AdeleRing, Prod.IsProdSMul, IsModuleTopology, ContinuousAlgEquiv, TensorProduct and 1 more
Proof uses: IsModuleTopology.continuousAlgEquivOfIsBiscalar, TensorProduct.RightActions.instAlgebra_fLT, NumberField.AdeleRing.baseChangeAlgEquiv
79 instances, coercions and auxiliary constants left out.
```
noncomputable def baseChangeEquiv [IsModuleTopology (𝔸 K) (𝔸 L)] :
    (L ⊗[K] 𝔸 K) ≃A[L] 𝔸 L :=
…
```
theorem NumberField.AdeleRing.baseChangeEquiv_tsum_apply_right line 195 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Algebra, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul, NumberField.InfiniteAdeleRing, Pi.FiberwiseSMul, NumberField.InfinitePlace, NumberField.InfinitePlace.comap, Algebra.algebraMap, NumberField.InfinitePlace.Completion, Subtype, Eq, NumberField.LiesOver.instAlgebraCompletion, NumberField.AdeleRing, Prod.IsProdSMul, IsModuleTopology, ContinuousAlgEquiv, TensorProduct and 5 more
Proof uses: HSMul.hSMul, of_eq_true, Eq.trans, True, congrArg, congrFun', mul_one, eq_self, congr, map_smul, RingHom.id, map_one, Algebra.algebraMap_eq_smul_one
138 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
abbrev NumberField.AdeleRing.tensorProductEquivPi A continuous K-linear isomorphism L ⊗[K] 𝔸_K = (𝔸_K)ⁿ for n = [L:K] line 206 source
Source documentation
A continuous K-linear isomorphism L ⊗[K] 𝔸_K = (𝔸_K)ⁿ for n = [L:K]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Algebra, ContinuousLinearEquiv, NumberField.AdeleRing, NumberField.RingOfIntegers, RingHom.id, TensorProduct, TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT, Fin, Module.finrank, TensorProduct.RightActions.instModule_fLT
Proof uses: LinearEquiv, TensorProduct.RightActions.instAlgebra_fLT, TensorProduct.RightActions.Algebra.TensorProduct.comm, TensorProduct.AlgebraTensorModule.finiteEquivPi, IsModuleTopology.continuousLinearEquiv, LinearEquiv.trans, LinearEquiv.symm
58 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev tensorProductEquivPi :
    L ⊗[K] (𝔸 K) ≃L[𝔸 K] (Fin (Module.finrank K L) → 𝔸 K) :=
…
```
abbrev NumberField.AdeleRing.piEquiv A continuous additive isomorphism (𝔸_K)ⁿ ≃ 𝔸_L for n = [L:K] line 220 source
Source documentation
A continuous additive isomorphism (𝔸_K)ⁿ ≃ 𝔸_L for n = [L:K]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Algebra, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul, NumberField.InfiniteAdeleRing, Pi.FiberwiseSMul, NumberField.InfinitePlace, NumberField.InfinitePlace.comap, Algebra.algebraMap, NumberField.InfinitePlace.Completion, Subtype, Eq, NumberField.LiesOver.instAlgebraCompletion, NumberField.AdeleRing, Prod.IsProdSMul, IsModuleTopology, ContinuousAddEquiv, Fin and 1 more
Proof uses: TensorProduct, TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT, ContinuousLinearEquiv.toContinuousAddEquiv, TensorProduct.RightActions.instModule_fLT, ContinuousLinearEquiv.symm, RingHom.id, NumberField.AdeleRing.tensorProductEquivPi, NumberField.AdeleRing.baseChangeEquiv, ContinuousAddEquiv.trans
84 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev piEquiv : (Fin (Module.finrank K L) → 𝔸 K) ≃ₜ+ 𝔸 L :=
…
```
theorem NumberField.AdeleRing.piEquiv_apply_of_algebraMap line 230 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Algebra, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul, NumberField.InfiniteAdeleRing, Pi.FiberwiseSMul, NumberField.InfinitePlace, NumberField.InfinitePlace.comap, Algebra.algebraMap, NumberField.InfinitePlace.Completion, Subtype, Eq, NumberField.LiesOver.instAlgebraCompletion, NumberField.AdeleRing, Prod.IsProdSMul, IsModuleTopology, Fin, Module.finrank and 7 more
Proof uses: Eq.mpr, ContinuousLinearEquiv, TensorProduct, TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT, NumberField.AdeleRing.baseChangeEquiv, TensorProduct.RightActions.instModule_fLT, LinearEquiv.trans, TensorProduct.RightActions.instAlgebra_fLT, TensorProduct.RightActions.Algebra.TensorProduct.comm, TensorProduct.AlgebraTensorModule.finiteEquivPi, id, congrFun', congrArg, Eq.trans, ContinuousLinearEquiv.toContinuousAddEquiv, Eq.symm, funext, ContinuousLinearEquiv.symm, NumberField.AdeleRing.tensorProductEquivPi, IsModuleTopology.continuousLinearEquiv_symm_apply and 12 more
176 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem NumberField.AdeleRing.piEquiv_mem_principalSubgroup line 242 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Algebra, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul, NumberField.InfiniteAdeleRing, Pi.FiberwiseSMul, NumberField.InfinitePlace, NumberField.InfinitePlace.comap, Algebra.algebraMap, NumberField.InfinitePlace.Completion, Subtype, Eq, NumberField.LiesOver.instAlgebraCompletion, NumberField.AdeleRing, Prod.IsProdSMul, IsModuleTopology, Fin, Module.finrank and 7 more
Proof uses: RingHom, Eq.rec, LinearEquiv, RingHom.id, LinearEquiv.symm, Module.Finite.equivPi, Exists.intro, rfl, Eq.symm, NumberField.AdeleRing.piEquiv_apply_of_algebraMap, Classical.choose, Eq.mp, Eq.trans, Set, forall_congr, True, implies_congr, Eq.refl, Classical.choose_spec
133 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem NumberField.AdeleRing.piEquiv_map_principalSubgroup line 253 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Algebra, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul, NumberField.InfiniteAdeleRing, Pi.FiberwiseSMul, NumberField.InfinitePlace, NumberField.InfinitePlace.comap, Algebra.algebraMap, NumberField.InfinitePlace.Completion, Subtype, Eq, NumberField.LiesOver.instAlgebraCompletion, NumberField.AdeleRing, Prod.IsProdSMul, IsModuleTopology, AddSubgroup, AddSubgroup.map and 7 more
Proof uses: AddSubgroup.ext, Eq.mpr, Iff, Membership.mem, Exists, And, id, congrFun', congrArg, Iff.intro, Eq.rec, NumberField.AdeleRing.piEquiv_mem_principalSubgroup, RingHom, Exists.intro, LinearEquiv, RingHom.id, Module.Finite.equivPi, And.intro, Set, rfl and 4 more
150 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem NumberField.AdeleRing.comap_piEquiv_principalSubgroup line 265 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Algebra, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul, NumberField.InfiniteAdeleRing, Pi.FiberwiseSMul, NumberField.InfinitePlace, NumberField.InfinitePlace.comap, Algebra.algebraMap, NumberField.InfinitePlace.Completion, Subtype, Eq, NumberField.LiesOver.instAlgebraCompletion, NumberField.AdeleRing, Prod.IsProdSMul, IsModuleTopology, AddSubgroup, Fin and 7 more
Proof uses: Eq.mpr, AddSubgroup.map, id, congrArg, Eq.symm, NumberField.AdeleRing.piEquiv_map_principalSubgroup, AddSubgroup.comap_map_eq_self_of_injective, ContinuousAddEquiv.injective, Eq.refl
102 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def NumberField.AdeleRing.piQuotientEquiv A continuous additive isomorphism (𝔸_K / K)ⁿ = 𝔸_L / L where n = [L:K] line 273 source
Source documentation
A continuous additive isomorphism (𝔸_K / K)ⁿ = 𝔸_L / L where n = [L:K].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Algebra, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul, NumberField.InfiniteAdeleRing, Pi.FiberwiseSMul, NumberField.InfinitePlace, NumberField.InfinitePlace.comap, Algebra.algebraMap, NumberField.InfinitePlace.Completion, Subtype, Eq, NumberField.LiesOver.instAlgebraCompletion, NumberField.AdeleRing, Prod.IsProdSMul, IsModuleTopology, ContinuousAddEquiv, Fin and 4 more
Proof uses: ContinuousAddEquiv.trans, AddSubgroup.pi, Set.univ, ContinuousAddEquiv.symm, ContinuousAddEquiv.quotientPi, QuotientAddGroup.continuousAddEquiv, NumberField.AdeleRing.piEquiv, NumberField.AdeleRing.piEquiv_map_principalSubgroup
99 instances, coercions and auxiliary constants left out.
```
noncomputable def piQuotientEquiv :
    (Fin (Module.finrank K L) → (𝔸 K) ⧸ principalSubgroup (𝓞 K) K) ≃ₜ+
      (𝔸 L) ⧸ principalSubgroup (𝓞 L) L :=
…
```
def NumberField.AdeleRing.ModuleBaseChangeLinearEquiv V ⊗[K] 𝔸_K = V ⊗[L] 𝔸_L as L-modules for V an L-module and K ⊆ L number fields line 290 source
Source documentation
V ⊗[K] 𝔸_K = V ⊗[L] 𝔸_L as L-modules for V an L-module and K ⊆ L number fields.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, AddCommGroup, Module, Algebra, IsScalarTower, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul, LinearEquiv, RingHom.id, TensorProduct, NumberField.AdeleRing
Proof uses: LinearEquiv.trans, TensorProduct.AlgebraTensorModule.congr, LinearEquiv.symm, TensorProduct.rid, LinearEquiv.refl, TensorProduct.AlgebraTensorModule.assoc, LinearEquiv.lTensor, NumberField.AdeleRing.baseChangeAlgEquiv
93 instances, coercions and auxiliary constants left out.
```
noncomputable def ModuleBaseChangeLinearEquiv :
    V ⊗[K] (𝔸 K) ≃ₗ[L] (V ⊗[L] (𝔸 L)) :=
…
```
theorem NumberField.AdeleRing.ModuleBaseChangeLinearEquiv_tmul_apply line 297 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, AddCommGroup, Module, Algebra, IsScalarTower, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul, NumberField.AdeleRing, Eq, TensorProduct, LinearEquiv, RingHom.id, NumberField.AdeleRing.ModuleBaseChangeLinearEquiv, TensorProduct.tmul, AlgEquiv, NumberField.AdeleRing.baseChangeAlgEquiv, OfNat.ofNat
Proof uses: rfl
95 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
instance NumberField.AdeleRing.(instance at line 304) line 304 source
def NumberField.AdeleRing.ModuleBaseChangeContinuousLinearEquiv 𝔸_K ⊗[K] V = 𝔸_L ⊗[L] V as topological additive groups for V an L-module and K ⊆ L number fields line 325 source
Source documentation
𝔸_K ⊗[K] V = 𝔸_L ⊗[L] V as topological additive groups for V an L-module and K ⊆ L number fields.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, AddCommGroup, Module, Algebra, IsScalarTower, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, IsDedekindDomain.FiniteAdeleRing.ComapFiberwiseSMul, FiniteDimensional, NumberField.InfiniteAdeleRing, NumberField.AdeleRing, Pi.FiberwiseSMul, NumberField.InfinitePlace, NumberField.InfinitePlace.comap, Algebra.algebraMap, NumberField.InfinitePlace.Completion, Subtype, Eq, NumberField.LiesOver.instAlgebraCompletion and 8 more
Proof uses: IsModuleTopology.continuousLinearEquivOfIsBiscalar, TensorProduct.RightActions.instModule_fLT, NumberField.AdeleRing.ModuleBaseChangeLinearEquiv
106 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
noncomputable def ModuleBaseChangeContinuousLinearEquiv
    [FiniteDimensional L V] [FiniteDimensional K V]
    [Algebra K∞ L∞] [Algebra (𝔸 K) (𝔸 L)]
    [Pi.FiberwiseSMul (fun a => a.comap (algebraMap K L)) Completion Completion]
    [Prod.IsProdSMul K∞ 𝔸ᶠ[K] L∞ 𝔸ᶠ[L]]
    [Module (𝔸 K) (V ⊗[L] 𝔸 L)] [IsScalarTower (𝔸 K) (𝔸 L) (V ⊗[L] 𝔸 L)]
    [IsModuleTopology (𝔸 K) (𝔸 L)] [Module.Finite (𝔸 K) (𝔸 L)] :
    V ⊗[K] (𝔸 K) ≃L[L] (V ⊗[L] (𝔸 L)) :=
…
```
Mentions: Pi.FiberwiseSMul, Prod.IsProdSMul
theorem Rat.AdeleRing.integral_and_norm_lt_one line 391 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Rat, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Membership.mem, IsDedekindDomain.HeightOneSpectrum.adicCompletion, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, IsDedekindDomain.FiniteAdeleRing, RingHom, Algebra.algebraMap, NumberField.InfinitePlace, LT.lt, Real, Norm.norm, NumberField.InfinitePlace.Completion, NumberField.InfiniteAdeleRing, OfNat.ofNat, Eq
Proof uses: id, WithAbs, AbsoluteValue, Exists, Complex, NumberField.place, Rat.infinitePlace, WithAbs.toAbs, Int, Subring, RingHom.range, IsDedekindDomain.HeightOneSpectrum.mem_integers_of_valuation_le_one, UniformSpace, WithZero, Multiplicative, IsDedekindDomain.HeightOneSpectrum.adicValued, Eq.mpr, LE.le, Valuation, IsDedekindDomain.HeightOneSpectrum.valuation and 34 more
176 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
theorem Rat.AdeleRing.zero_discrete line 421 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, Set, NumberField.AdeleRing, NumberField.RingOfIntegers, Rat, And, IsOpen, Eq, Set.preimage, RingHom, Algebra.algebraMap, Singleton.singleton, OfNat.ofNat
Proof uses: IsDedekindDomain.FiniteAdeleRing, Set.ofPred, IsDedekindDomain.HeightOneSpectrum, Membership.mem, IsDedekindDomain.HeightOneSpectrum.adicCompletion, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Exists.intro, SProd.sprod, NumberField.InfiniteAdeleRing, Prod, NumberField.InfinitePlace, NumberField.InfinitePlace.Completion, Metric.ball, Real, And.intro, IsOpen.prod, Eq.mpr, Set.iInter, id and 36 more
137 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
theorem NumberField.AdeleRing.zero_discrete line 464 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Exists, Set, NumberField.AdeleRing, NumberField.RingOfIntegers, And, IsOpen, Eq, Set.preimage, RingHom, Algebra.algebraMap, Singleton.singleton, OfNat.ofNat
Proof uses: Rat, Rat.AdeleRing.zero_discrete, Exists.intro, Set.image, Fin, Module.finrank, ContinuousAddEquiv, NumberField.AdeleRing.piEquiv, Set.ofPred, Membership.mem, And.intro, Eq.mpr, Homeomorph, ContinuousAddEquiv.toHomeomorph, id, congrArg, Eq.symm, ContinuousAddEquiv.coe_toHomeomorph, propext, Homeomorph.isOpen_image and 22 more
137 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
theorem NumberField.AdeleRing.discrete line 494 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Exists, Set, NumberField.AdeleRing, NumberField.RingOfIntegers, And, IsOpen, Eq, Set.preimage, RingHom, Algebra.algebraMap, Singleton.singleton
Proof uses: OfNat.ofNat, NumberField.AdeleRing.zero_discrete, rfl, Homeomorph, Homeomorph.subLeft, Exists.intro, And.intro, Iff.mpr, Homeomorph.isOpen_preimage, Function.comp, Equiv, Equiv.subLeft, funext, of_eq_true, Eq.trans, HSub.hSub, True, congr, congrArg, congrFun' and 12 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
instance Rat.FiniteAdeleRing.(instance at line 523) line 523 source
def Rat.FiniteAdeleRing.padicEquiv line 531 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AlgEquiv, Rat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, RestrictedProduct, Nat.Primes, Padic, Nat, Nat.Prime, Rat.FiniteAdeleRing.instFactPrimeValNat, Subring, PadicInt.subring, Filter.cofinite
Proof uses: RingEquiv, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.adicCompletion, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, RingEquiv.restrictedProductCongr, Rat.HeightOneSpectrum.primesEquiv, AlgEquiv.toRingEquiv, Equiv, ContinuousAlgEquiv.toAlgEquiv, Rat.HeightOneSpectrum.adicCompletion.padicEquiv, AlgEquiv.mk, RingEquiv.toEquiv
80 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
theorem Rat.FiniteAdeleRing.padicEquiv_bijOn line 551 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set.BijOn, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Rat, RestrictedProduct, Nat.Primes, Padic, Nat, Nat.Prime, Rat.FiniteAdeleRing.instFactPrimeValNat, Subring, PadicInt.subring, Filter.cofinite, AlgEquiv, Rat.FiniteAdeleRing.padicEquiv, IsDedekindDomain.FiniteAdeleRing.integralAdeles, Subtype, RestrictedProduct.structureSubring
Proof uses: RingEquiv.restrictedProductCongr_bijOn_structureSubring, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.adicCompletion, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Rat.HeightOneSpectrum.primesEquiv, Eq.symm, Filter, Filter.comap, Equiv, Function.Injective.comap_cofinite_eq, Equiv.injective, AlgEquiv.toRingEquiv, ContinuousAlgEquiv.toAlgEquiv, Rat.HeightOneSpectrum.adicCompletion.padicEquiv, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn
66 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Rat.FiniteAdeleRing.sub_mem_integralAdeles line 562 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Rat, Exists, Membership.mem, Subring, IsDedekindDomain.FiniteAdeleRing.integralAdeles, HSub.hSub, RingHom, Algebra.algebraMap
Proof uses: RestrictedProduct, Nat.Primes, Padic, Nat, Nat.Prime, RestrictedProduct.instFactPrimeValNat_fLT, PadicInt.subring, Filter.cofinite, Subtype, RestrictedProduct.structureSubring, AlgEquiv, Rat.FiniteAdeleRing.instFactPrimeValNat, Rat.FiniteAdeleRing.padicEquiv, RestrictedProduct.padic_exists_sub_mem_structureSubring, Exists.intro, Eq.mpr, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.adicCompletion, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers and 23 more
92 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Rat.InfiniteAdeleRing.exists_unique_sub_mem_Ico line 572 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NumberField.InfiniteAdeleRing, Rat, ExistsUnique, NumberField.RingOfIntegers, NumberField.InfinitePlace, Membership.mem, Real, Set, Set.Ico, OfNat.ofNat, RingHom, NumberField.InfinitePlace.Completion, NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal, Rat.infinitePlace_isReal, HSub.hSub, Algebra.algebraMap
Proof uses: Rat.infinitePlace, Rat.isReal_infinitePlace, Int, Int.floor, Exists.intro, And, Eq, RingEquiv, RingEquiv.symm, Rat.ringOfIntegersEquiv, And.intro, Eq.mpr, id, congrArg, Subsingleton.elim, NumberField.InfinitePlace.Completion.ofCompletion, WithAbs, AbsoluteValue, Exists, Complex and 24 more
97 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
theorem Rat.InfiniteAdeleRing.exists_sub_norm_le_one line 595 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NumberField.InfiniteAdeleRing, Rat, Exists, NumberField.RingOfIntegers, NumberField.InfinitePlace, LE.le, Real, Norm.norm, NumberField.InfinitePlace.Completion, HSub.hSub, RingHom, Algebra.algebraMap, OfNat.ofNat
Proof uses: And, Membership.mem, Set, Set.Ico, NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal, Rat.infinitePlace_isReal, Eq, ExistsUnique, Rat.InfiniteAdeleRing.exists_unique_sub_mem_Ico, Exists.intro, forall_imp, Eq.mpr, Rat.infinitePlace, id, congrArg, Subsingleton.elim, Rat.isReal_infinitePlace, Eq.symm, Isometry.norm_map_of_map_zero, NumberField.InfinitePlace.Completion.isometry_extensionEmbeddingOfIsReal and 4 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
instance (instance at line 605) line 605 source
theorem Rat.AdeleRing.cocompact line 610 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CompactSpace, HasQuotient.Quotient, NumberField.AdeleRing, NumberField.RingOfIntegers, Rat, AddSubgroup, NumberField.AdeleRing.principalSubgroup
Proof uses: CompactSpace.mk, Set, Set.prod, NumberField.InfinitePlace, NumberField.InfinitePlace.Completion, IsDedekindDomain.FiniteAdeleRing, Set.pi, Set.univ, Metric.closedBall, OfNat.ofNat, Real, Subring, IsDedekindDomain.FiniteAdeleRing.integralAdeles, IsCompact, IsCompact.prod, isCompact_univ_pi, Iff.mpr, And, IsClosed, Bornology.IsBounded and 84 more
153 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
def Rat.AdeleRing.fundamentalDomain The fundamental domain ℤ^ x [0,1) for 𝔸_ℚ ⧸ ℚ line 637 source
Source documentation
The fundamental domain ℤ^ x [0,1) for 𝔸_ℚ ⧸ ℚ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, NumberField.AdeleRing, NumberField.RingOfIntegers, Rat
Proof uses: Set.prod, NumberField.InfinitePlace, NumberField.InfinitePlace.Completion, IsDedekindDomain.FiniteAdeleRing, Set.pi, Set.univ, Set.preimage, Real, OneHom.toFun, NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal, Rat.infinitePlace_isReal, Set.Ico, OfNat.ofNat, Set.range, IsDedekindDomain.HeightOneSpectrum, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers and 2 more
40 instances, coercions and auxiliary constants left out.
```
def Rat.AdeleRing.fundamentalDomain : Set (AdeleRing (𝓞 ℚ) ℚ) :=
…
```
def FiniteAdeleRing.toAdicCompletion The canonical ring homomorphism from the finite adele ring to a nonarchimedean local factor line 643 source
Source documentation
The canonical ring homomorphism from the finite adele ring to a nonarchimedean local factor.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, RingHom, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.HeightOneSpectrum.adicCompletion
Proof uses: RingHom.mk, MonoidHom.mk, OneHom.mk
32 instances, coercions and auxiliary constants left out.
```
def FiniteAdeleRing.toAdicCompletion {K : Type*} [Field K] [NumberField K]
    (v : HeightOneSpectrum (𝓞 K)) :
    𝔸ᶠ[K] →+* v.adicCompletion K where
…
```
instance (instance at line 655) line 655 source
instance (instance at line 657) line 657 source
lemma Rat.AdeleRing.mem_fundamentalDomain bleurgh line 661 source
Source comment
bleurgh

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NumberField.AdeleRing, NumberField.RingOfIntegers, Rat, Exists, Membership.mem, Set, Rat.AdeleRing.fundamentalDomain, HAdd.hAdd, RingHom, Algebra.algebraMap
Proof uses: IsDedekindDomain.FiniteAdeleRing, Subring, IsDedekindDomain.FiniteAdeleRing.integralAdeles, HSub.hSub, Prod.snd, NumberField.InfiniteAdeleRing, Rat.FiniteAdeleRing.sub_mem_integralAdeles, IsDedekindDomain.HeightOneSpectrum, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Eq, IsDedekindDomain.FiniteAdeleRing.structureMap, And, NumberField.InfinitePlace, Real, Set.Ico, OfNat.ofNat, NumberField.InfinitePlace.Completion and 56 more
120 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
lemma Rat.AdeleRing.mem_fundamentalDomain (a : AdeleRing (𝓞 ℚ) ℚ) :
    ∃ g, algebraMap ℚ (AdeleRing (𝓞 ℚ) ℚ) g + a ∈ fundamentalDomain := by
…
```
Mentions: Rat.AdeleRing.fundamentalDomain
lemma Rat.AdeleRing.fundamentalDomain_traversal Documented declaration: fundamentalDomain_traversal line 695 source
Source comment
this uses the same techniques as `Rat.AdeleRing.zero_discrete` which should be a corollary: fundamentalDomain - fundamentalDomain ⊆ the U used in the proof This lemma is in fact a "concrete version" of that one

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NumberField.AdeleRing, NumberField.RingOfIntegers, Rat, Membership.mem, Set, Rat.AdeleRing.fundamentalDomain, Eq, HAdd.hAdd, RingHom, Algebra.algebraMap, OfNat.ofNat
Proof uses: Rat.AdeleRing.integral_and_norm_lt_one, IsDedekindDomain.HeightOneSpectrum, Eq.mpr, IsDedekindDomain.HeightOneSpectrum.adicCompletion, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, IsDedekindDomain.FiniteAdeleRing, HSub.hSub, Prod, NumberField.InfiniteAdeleRing, RingHom.snd, id, congrArg, Eq.mp, RingHom.map_rat_algebraMap, Eq.symm, propext, eq_sub_iff_add_eq, map_add, eq_of_heq and 97 more
167 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
```
lemma Rat.AdeleRing.fundamentalDomain_traversal {a b : AdeleRing (𝓞 ℚ) ℚ}
    (ha : a ∈ fundamentalDomain) (hb : b ∈ fundamentalDomain) {q : ℚ}
    (hq : algebraMap _ _ q + a = b) : q = 0 := by
…
```
Mentions: Rat.AdeleRing.fundamentalDomain
instance (instance at line 741) line 741 source
theorem Rat.AdeleRing.isAddFundamentalDomain line 746 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.IsAddFundamentalDomain, Rat, NumberField.AdeleRing, NumberField.RingOfIntegers, NumberField.InfinitePlace, NumberField.InfinitePlace.Completion, IsDedekindDomain.FiniteAdeleRing, Rat.AdeleRing.fundamentalDomain, MeasureTheory.Measure.prod, MeasureTheory.Measure.pi, MeasureTheory.Measure.addHaar
Proof uses: MeasureTheory.IsAddFundamentalDomain.mk, MeasureTheory.NullMeasurableSet.prod, Classical.arbitrary, TopologicalSpace.PositiveCompacts, Set.pi, Set.univ, Set.preimage, Real, OneHom.toFun, NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal, Rat.infinitePlace_isReal, Set.Ico, OfNat.ofNat, Set.range, IsDedekindDomain.HeightOneSpectrum, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers and 99 more
207 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
theorem NumberField.AdeleRing.cocompact line 788 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CompactSpace, HasQuotient.Quotient, NumberField.AdeleRing, NumberField.RingOfIntegers, AddSubgroup, NumberField.AdeleRing.principalSubgroup
Proof uses: Homeomorph.compactSpace, Fin, Module.finrank, Rat, Rat.AdeleRing.cocompact, ContinuousAddEquiv.toHomeomorph, NumberField.AdeleRing.piQuotientEquiv
48 instances, coercions and auxiliary constants left out.
def NumberField.AdeleRing.baseChangeAdeleAlgHom The canonical 𝔸 K-algebra homomorphism (L ⊗_K 𝔸 K) → 𝔸 L induced by the maps from L and 𝔸 K into 𝔸 L line 821 source
Source documentation
The canonical 𝔸 K-algebra homomorphism (L ⊗_K 𝔸 K) → 𝔸 L induced by the maps from L and 𝔸 K into 𝔸 L.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Algebra, AlgHom, NumberField.AdeleRing, NumberField.RingOfIntegers, TensorProduct, TensorProduct.RightActions.instAlgebra_fLT
Proof uses: SemialgHom.baseChangeRightOfAlgebraMap, ContinuousSemialgHom.toSemialgHom, Algebra.algebraMap, NumberField.AdeleRing.baseChange
25 instances, coercions and auxiliary constants left out.
```
noncomputable def baseChangeAdeleAlgHom : (L ⊗[K] (𝔸 K)) →ₐ[𝔸 K] 𝔸 L :=
…
```
lemma NumberField.AdeleRing.baseChangeAdeleAlgHom_bijective line 824 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Algebra, Function.Bijective, TensorProduct, NumberField.AdeleRing, NumberField.RingOfIntegers, AlgHom, TensorProduct.RightActions.instAlgebra_fLT, NumberField.AdeleRing.baseChangeAdeleAlgHom
Proof uses: LinearEquiv, RingHom.id, Prod, NumberField.InfiniteAdeleRing, IsDedekindDomain.FiniteAdeleRing, TensorProduct.prodRight, LinearEquiv.prodCongr, NumberField.InfiniteAdeleRing.baseChangeAlgEquiv, IsDedekindDomain.FiniteAdeleRing.baseChangeAlgEquiv, LinearEquiv.trans, Eq, funext, TensorProduct.inductionOn, Eq.refl, TensorProduct.tmul, of_eq_true, HAdd.hAdd, Eq.trans, True, congr and 7 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def NumberField.AdeleRing.baseChangeAlgAdeleEquiv The canonical 𝔸_K-algebra isomorphism from L ⊗_K 𝔸_K to 𝔸_L induced by the base change map 𝔸_K → 𝔸_L line 842 source
Source documentation
The canonical 𝔸_K-algebra isomorphism from L ⊗_K 𝔸_K to 𝔸_L induced by the base change map 𝔸_K → 𝔸_L.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Algebra, AlgEquiv, NumberField.AdeleRing, NumberField.RingOfIntegers, TensorProduct, TensorProduct.RightActions.instAlgebra_fLT
Proof uses: AlgEquiv.ofBijective, NumberField.AdeleRing.baseChangeAdeleAlgHom, NumberField.AdeleRing.baseChangeAdeleAlgHom_bijective
28 instances, coercions and auxiliary constants left out.
```
noncomputable def baseChangeAlgAdeleEquiv : (L ⊗[K] 𝔸 K) ≃ₐ[𝔸 K] 𝔸 L :=
…
```
def NumberField.AdeleRing.baseChangeAdeleEquiv The canonical 𝔸_K-algebra homeomorphism from L ⊗_K 𝔸_K to 𝔸_L induced by the base change map 𝔸_K → 𝔸_L line 847 source
Source documentation
The canonical 𝔸_K-algebra homeomorphism from L ⊗_K 𝔸_K to 𝔸_L induced by the base change map 𝔸_K → 𝔸_L.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Algebra, ContinuousAlgEquiv, NumberField.AdeleRing, NumberField.RingOfIntegers, TensorProduct, TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT, TensorProduct.RightActions.instAlgebra_fLT
Proof uses: IsModuleTopology.continuousAlgEquivOfAlgEquiv, NumberField.AdeleRing.baseChangeAlgAdeleEquiv
34 instances, coercions and auxiliary constants left out.
```
noncomputable def baseChangeAdeleEquiv : (L ⊗[K] 𝔸 K) ≃A[𝔸 K] 𝔸 L :=
…
```
def NumberField.AdeleRing.baseChangeEquiv' The canonical L-algebra isomorphism from L ⊗_K 𝔸_K to 𝔸_L induced by the K-algebra base change map 𝔸_K → 𝔸_L line 852 source
Source documentation
The canonical L-algebra isomorphism from L ⊗_K 𝔸_K to 𝔸_L induced by the K-algebra base change map 𝔸_K → 𝔸_L.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Algebra, ContinuousAlgEquiv, TensorProduct, NumberField.AdeleRing, NumberField.RingOfIntegers, TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT
Proof uses: AlgHom, SemialgHom.baseChangeOfAlgebraMap, ContinuousSemialgHom.toSemialgHom, Algebra.algebraMap, NumberField.AdeleRing.baseChange, TensorProduct.RightActions.instAlgebra_fLT, NumberField.AdeleRing.baseChangeAdeleEquiv, ContinuousAlgEquiv.mk, AlgEquiv.mk, Equiv.mk, OneHom.toFun, AlgHom.toRingHom, Equiv.invFun, AlgEquiv.toEquiv, ContinuousAlgEquiv.toAlgEquiv
51 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
noncomputable def baseChangeEquiv' :
    (L ⊗[K] 𝔸 K) ≃A[L] 𝔸 L where
…
```
example NumberField.AdeleRing.(example at line 858) line 858 source
Source comment
this isn't rfl. Explanation below
```
example (x : L ⊗[K] 𝔸 K) : baseChangeEquiv K L x = baseChangeEquiv' K L x := by
…
```
Mentions: NumberField.AdeleRing.baseChangeEquiv, NumberField.AdeleRing.baseChangeEquiv'