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

104 declarations, 0 contain sorry, 0 declared as axioms

Finiteness theorem for the adelic quotient of a division algebra

Let D be a finite-dimensional division algebra over a number field K. Setup and intermediate results towards the classical theorem that the adelic double-coset space D^× \ (D ⊗ 𝔸_K)^× / U is finite for any compact open subgroup U.

Imports (23)

Imported by 2 files

abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.Df Df is notation for D ⊗ 𝔸_K^∞ line 90 source
Source documentation
Df is notation for D ⊗ 𝔸_K^∞
```
abbrev Df := D ⊗[K] (FiniteAdeleRing (𝓞 K) K)
```
abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.Dfx Dfx is notation for (D ⊗ 𝔸_K^∞)ˣ line 93 source
Source documentation
Dfx is notation for (D ⊗ 𝔸_K^∞)ˣ.
```
abbrev Dfx := (Df K D)ˣ
```
Mentions: NumberField.AdeleRing.DivisionAlgebra.Aux.Df
abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.Dinf Dinf is notation for D ⊗ 𝔸_K^∞ line 96 source
Source documentation
Dinf is notation for D ⊗ 𝔸_K^∞
```
abbrev Dinf := D ⊗[K] (NumberField.InfiniteAdeleRing K)
```
abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.Dinfx Dinfx is notation for (D ⊗ 𝔸_K^∞)ˣ line 99 source
Source documentation
Dinfx is notation for (D ⊗ 𝔸_K^∞)ˣ
```
abbrev Dinfx := (Dinf K D)ˣ
```
Mentions: NumberField.AdeleRing.DivisionAlgebra.Aux.Dinf
abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.incl The inclusion Dˣ → D_𝔸ˣ as a group homomorphism line 102 source
Source documentation
The inclusion Dˣ → D_𝔸ˣ as a group homomorphism.
```
abbrev incl : Dˣ →* D_𝔸ˣ :=
…
```
abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.incl₁ The inclusion Dˣ → (D ⊗ 𝔸_K^∞)ˣ as a group homomorphism line 106 source
Source documentation
The inclusion Dˣ → (D ⊗ 𝔸_K^∞)ˣ as a group homomorphism.
```
noncomputable abbrev incl₁ : Dˣ →* Dfx K D :=
…
```
Mentions: NumberField.AdeleRing.DivisionAlgebra.Aux.Dfx
abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.inclKn𝔸Kn The inclusion of K^n into 𝔸^n line 110 source
Source documentation
The inclusion of K^n into 𝔸^n.
```
abbrev inclKn𝔸Kn : (Fin (Module.finrank K D) → K) →
    (Fin (Module.finrank K D) → AdeleRing (𝓞 K) K) :=
…
```
instance NumberField.AdeleRing.DivisionAlgebra.Aux.(instance at line 119) line 119 source
Source documentation
The ℝ-algebra structure on Dinf K D.
```
instance : Algebra ℝ (Dinf K D) :=
…
```
Mentions: NumberField.AdeleRing.DivisionAlgebra.Aux.Dinf
instance NumberField.AdeleRing.DivisionAlgebra.Aux.(instance at line 125) line 125 source
instance NumberField.AdeleRing.DivisionAlgebra.Aux.(instance at line 131) line 131 source
Source documentation
We put the Borel measurable space structure on D_𝔸 in this file.
```
instance : MeasurableSpace D_𝔸 := borel _
```
instance NumberField.AdeleRing.DivisionAlgebra.Aux.(instance at line 133) line 133 source
instance NumberField.AdeleRing.DivisionAlgebra.Aux.(instance at line 135) line 135 source
instance NumberField.AdeleRing.DivisionAlgebra.Aux.(instance at line 139) line 139 source
Source documentation
Dinf K D has the ℝ-module topology.
```
instance : IsModuleTopology ℝ (Dinf K D) := by
…
```
Mentions: NumberField.AdeleRing.DivisionAlgebra.Aux.Dinf
instance NumberField.AdeleRing.DivisionAlgebra.Aux.(instance at line 148) line 148 source
Source documentation
Dinf K D is given the borel sigma algebra (for Haar measure).
```
instance : MeasurableSpace (Dinf K D) := borel (Dinf K D)
```
Mentions: NumberField.AdeleRing.DivisionAlgebra.Aux.Dinf
instance NumberField.AdeleRing.DivisionAlgebra.Aux.(instance at line 150) line 150 source
instance NumberField.AdeleRing.DivisionAlgebra.Aux.(instance at line 153) line 153 source
Source documentation
Df K D is given the borel sigma algebra (for Haar measure).
```
instance : MeasurableSpace (Df K D) := borel (Df K D)
```
Mentions: NumberField.AdeleRing.DivisionAlgebra.Aux.Df
instance NumberField.AdeleRing.DivisionAlgebra.Aux.(instance at line 155) line 155 source
instance NumberField.AdeleRing.DivisionAlgebra.Aux.(instance at line 158) line 158 source
Source comment
D ⊗ K_∞ is second countable because it's a finite ℝ-module
```
instance : SecondCountableTopology (Dinf K D) :=
…
```
Mentions: NumberField.AdeleRing.DivisionAlgebra.Aux.Dinf
theorem NumberField.AdeleRing.DivisionAlgebra.Aux.Kn_discrete line 163 source
abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.DIso The K-algebra equivalence of D and K^n line 170 source
Source documentation
The K-algebra equivalence of D and K^n.
```
abbrev DIso : (D ≃ₗ[K] ((Fin (Module.finrank K D) → K))) := Module.Finite.equivPi K D
…
```
Mentions: Module.Finite.equivPi

example NumberField.AdeleRing.DivisionAlgebra.Aux.(example at line 176) line 176 source

Source comment

...makes this work

example : IsModuleTopology (AdeleRing (𝓞 K) K)
    ((Fin (Module.finrank K D) → AdeleRing (𝓞 K) K)) := inferInstance

abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸Iso The 𝔸_K-algebra equivalence of D_𝔸 and 𝔸_K^d line 180 source
Source documentation
The 𝔸_K-algebra equivalence of D_𝔸 and 𝔸_K^d.
```
abbrev D𝔸Iso : (D_𝔸 ≃ₗ[(AdeleRing (𝓞 K) K)] ((Fin (Module.finrank K D) → AdeleRing (𝓞 K) K))) :=
…
```
abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸IsoTop The topological 𝔸_K-linear equivalence D_𝔸 ≃ 𝔸_K^d line 185 source
Source documentation
The topological 𝔸_K-linear equivalence D_𝔸 ≃ 𝔸_K^d.
```
abbrev D𝔸IsoTop : D_𝔸 ≃L[(AdeleRing (𝓞 K) K)]
    ((Fin (Module.finrank K D) → AdeleRing (𝓞 K) K)) :=
…
```
theorem NumberField.AdeleRing.DivisionAlgebra.Aux.D_discrete_aux line 189 source
theorem NumberField.AdeleRing.DivisionAlgebra.Aux.D_discrete line 205 source
def NumberField.AdeleRing.DivisionAlgebra.Aux.includeLeftSubgroup The additive subgroup D of D_𝔸 line 214 source
Source documentation
The additive subgroup D of D_𝔸.
```
def includeLeftSubgroup : AddSubgroup D_𝔸 :=
…
```
instance NumberField.AdeleRing.DivisionAlgebra.Aux.discrete_includeLeft_subgroup line 217 source
instance NumberField.AdeleRing.DivisionAlgebra.Aux.(instance at line 232) line 232 source
instance NumberField.AdeleRing.DivisionAlgebra.Aux.discrete_principalSubgroup line 234 source
instance NumberField.AdeleRing.DivisionAlgebra.Aux.compact_includeLeft_subgroup we seem to have this twice? line 249 source
Source comment
we seem to have this twice?
```
instance compact_includeLeft_subgroup :
    CompactSpace (D_𝔸 ⧸ (includeLeftSubgroup K D)) := by
…
```
Mentions: NumberField.AdeleRing.DivisionAlgebra.Aux.includeLeftSubgroup
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.not_injective_of_large_measure line 296 source
abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸ProdRight The K-algebra isomorphism D_𝔸 ≃ D_∞ × D_f -- adelic D is infinite adele D times finite adele D line 311 source
Source documentation
The K-algebra isomorphism D_𝔸 ≃ D_∞ × D_f -- adelic D is infinite adele D times finite adele D.
```
abbrev D𝔸ProdRight : D_𝔸 ≃ₐ[K] Dinf K D × Df K D :=
…
```
Mentions: NumberField.AdeleRing.DivisionAlgebra.Aux.Dinf, NumberField.AdeleRing.DivisionAlgebra.Aux.Df
instance NumberField.AdeleRing.DivisionAlgebra.Aux.(instance at line 315) line 315 source
Source documentation
The (InfiniteAdeleRing K × FiniteAdeleRing (𝓞 K) K)-module structure on (Dinf K D × Df K D).
```
instance : Module (AdeleRing (𝓞 K) K) (Dinf K D × Df K D) where
…
```
Mentions: NumberField.AdeleRing.DivisionAlgebra.Aux.Dinf, NumberField.AdeleRing.DivisionAlgebra.Aux.Df
instance NumberField.AdeleRing.DivisionAlgebra.Aux.(instance at line 334) line 334 source
Source documentation
(Dinf K D × Df K D) has the 𝔸_K module topology.
```
instance : IsModuleTopology (AdeleRing (𝓞 K) K) (Dinf K D × Df K D) :=
…
```
Mentions: NumberField.AdeleRing.DivisionAlgebra.Aux.Dinf, NumberField.AdeleRing.DivisionAlgebra.Aux.Df
abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸ProdRight' The 𝔸_K linear map D_𝔸 ≃ D_∞ × D_f line 338 source
Source documentation
The 𝔸_K linear map D_𝔸 ≃ D_∞ × D_f.
```
abbrev D𝔸ProdRight' : D_𝔸 ≃ₗ[AdeleRing (𝓞 K) K] (Dinf K D × Df K D) := {
…
```
Mentions: NumberField.AdeleRing.DivisionAlgebra.Aux.Dinf, NumberField.AdeleRing.DivisionAlgebra.Aux.Df
abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸ProdRight'' The continuous additive isomorphism D_𝔸 ≃ D_∞ × D_f line 354 source
Source documentation
The continuous additive isomorphism D_𝔸 ≃ D_∞ × D_f.
```
abbrev D𝔸ProdRight'' : D_𝔸 ≃ₜ+ Dinf K D × Df K D where
…
```
Mentions: NumberField.AdeleRing.DivisionAlgebra.Aux.Dinf, NumberField.AdeleRing.DivisionAlgebra.Aux.Df
abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸ProdRightUnits The equivalence of the units of D_𝔸 and the product of the units of (D ⊗ 𝔸_K^f) and (D ⊗ 𝔸_K^∞) line 361 source
Source documentation
The equivalence of the units of D_𝔸 and the product of the units of (D ⊗ 𝔸_K^f) and (D ⊗ 𝔸_K^∞).
```
abbrev D𝔸ProdRightUnits : D_𝔸ˣ ≃* (Dinfx K D) × (Dfx K D) :=
…
```
Mentions: NumberField.AdeleRing.DivisionAlgebra.Aux.Dinfx, NumberField.AdeleRing.DivisionAlgebra.Aux.Dfx
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.smul_D𝔸_prodRight_symm line 365 source
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸_prodRight_units_cont line 371 source
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.ringHaarChar_D𝔸 line 384 source
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.ringHaarChar_D𝔸_real_surjective For any positive real r, there's some ρ ∈ ℝˣ such that the haar character of (ρ, 1) ∈ D_f × D_∞ is r line 393 source
Source documentation
For any positive real r, there's some ρ ∈ ℝˣ such that the haar character of (ρ, 1) ∈ D_f × D_∞ is r.
```
lemma ringHaarChar_D𝔸_real_surjective (r : ℝ) (h : r > 0) :
    ∃ (ρ : ℝˣ), ringHaarChar
      ((D𝔸ProdRightUnits K D).symm (((Units.map (algebraMap ℝ (Dinf K D))) ρ),1)) = r := by
…
```
Mentions: NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸ProdRightUnits, NumberField.AdeleRing.DivisionAlgebra.Aux.Dinf
instance NumberField.InfiniteAdeleRing.(instance at line 423) line 423 source
lemma NumberField.InfiniteAdeleRing.isCentralSimple_infinite_addHaarScalarFactor_left_mul_eq_right_mul_aux Left and right Haar characters agree for u : (Π vi : InfinitePlace K, (D ⊗[K] vi.Completion))ˣ line 431 source
Source documentation
Left and right Haar characters agree for u : (Π vi : InfinitePlace K, (D ⊗[K] vi.Completion))ˣ.
```
lemma isCentralSimple_infinite_addHaarScalarFactor_left_mul_eq_right_mul_aux
    [Algebra.IsCentral K D] (u : (Π vi : InfinitePlace K, (D ⊗[K] vi.Completion))ˣ) :
    addEquivAddHaarChar (ContinuousAddEquiv.mulLeft u) =
    addEquivAddHaarChar (ContinuousAddEquiv.mulRight u) := by
…
```
def NumberField.InfiniteAdeleRing.realToCompletion The canonical ℝ-algebra structure on InfinitePlace.Completion line 462 source
Source documentation
The canonical ℝ-algebra structure on InfinitePlace.Completion.
```
def realToCompletion (vi : InfinitePlace K) : ℝ →+* vi.Completion :=
…
```
instance NumberField.InfiniteAdeleRing.(instance at line 469) line 469 source
lemma NumberField.InfiniteAdeleRing.algebraMap_completion_def line 473 source
instance NumberField.InfiniteAdeleRing.(instance at line 476) line 476 source
instance NumberField.InfiniteAdeleRing.(instance at line 493) line 493 source
instance NumberField.InfiniteAdeleRing.(instance at line 503) line 503 source
instance NumberField.InfiniteAdeleRing.(instance at line 506) line 506 source
instance NumberField.InfiniteAdeleRing.(instance at line 509) line 509 source
instance NumberField.InfiniteAdeleRing.(instance at line 512) line 512 source
instance NumberField.InfiniteAdeleRing.(instance at line 516) line 516 source
lemma NumberField.InfiniteAdeleRing.algebraMap_completion line 521 source
lemma NumberField.InfiniteAdeleRing.tensorPi_equiv_piTensor_map_mul line 536 source
def NumberField.InfiniteAdeleRing.DinfTensorPiEquivPiTensorAux tensorPiEquivPiTensor applied to Dinf, as a ℝ-linear equiv line 553 source
Source documentation
tensorPiEquivPiTensor applied to Dinf, as a ℝ-linear equiv.
```
def DinfTensorPiEquivPiTensorAux :
    (Dinf K D) ≃ₗ[ℝ] Π vi : InfinitePlace K, (D ⊗[K] vi.Completion) := {
…
```
def NumberField.InfiniteAdeleRing.DinfTensorPiEquivPiTensor tensorPiEquivPiTensor applied to Dinf, as a continuous ℝ-linear equiv line 572 source
Source documentation
tensorPiEquivPiTensor applied to Dinf, as a continuous ℝ-linear equiv.
```
def DinfTensorPiEquivPiTensor :
    (Dinf K D) ≃L[ℝ] Π vi : InfinitePlace K, (D ⊗[K] vi.Completion) := {
…
```
def NumberField.InfiniteAdeleRing.DinfTensorPiEquivPiTensorMulEquiv tensorPiEquivPiTensor applied to Dinf, as a mul equiv line 582 source
Source documentation
tensorPiEquivPiTensor applied to Dinf, as a mul equiv.
```
def DinfTensorPiEquivPiTensorMulEquiv :
    (Dinf K D) ≃* Π vi : InfinitePlace K, (D ⊗[K] vi.Completion) := {
…
```
lemma NumberField.InfiniteAdeleRing.isCentralSimple_infinite_addHaarScalarFactor_left_mul_eq_right_mul line 589 source
depends on sorry (Lean reported 10 error(s) in this file) what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, FiniteDimensional, Algebra.IsCentral, Units, NumberField.AdeleRing.DivisionAlgebra.Aux.Dinf, NumberField.InfiniteAdeleRing, Eq, NNReal, MeasureTheory.addEquivAddHaarChar, TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT, TensorProduct.RightActions.instIsTopologicalAddGroup_fLT, TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT, ContinuousAddEquiv.mulLeft, TensorProduct.RightActions.instIsTopologicalRing_fLT_1, ContinuousAddEquiv.mulRight
Proof uses: NumberField.InfinitePlace, MeasurableSpace, TensorProduct, NumberField.InfinitePlace.Completion, Real, AbsoluteValue, Exists, RingHom, Complex, NumberField.place, borel, BorelSpace, BorelSpace.mk, rfl, sorryAx, Lean.Name, Bool.true, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous and 2 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma NumberField.AdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul line 634 source
depends on sorry (Lean reported 10 error(s) in this file) what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, FiniteDimensional, Algebra.IsCentral, Units, TensorProduct, NumberField.AdeleRing, NumberField.RingOfIntegers, Eq, NNReal, MeasureTheory.addEquivAddHaarChar, TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT, TensorProduct.RightActions.instIsTopologicalAddGroup_fLT, TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT, ContinuousAddEquiv.mulLeft, TensorProduct.RightActions.instIsTopologicalRing_fLT_1, ContinuousAddEquiv.mulRight
Proof uses: Prod, NumberField.AdeleRing.DivisionAlgebra.Aux.Dinfx, NumberField.AdeleRing.DivisionAlgebra.Aux.Dfx, MulEquiv, NumberField.AdeleRing.DivisionAlgebra.Aux.Dinf, NumberField.InfiniteAdeleRing, NumberField.AdeleRing.DivisionAlgebra.Aux.Df, IsDedekindDomain.FiniteAdeleRing, NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸ProdRightUnits, HMul.hMul, Prod.fst, Prod.snd, Eq.mpr, ContinuousAddEquiv.sumCongr, id, congrArg, Eq.symm, MeasureTheory.addEquivAddHaarChar_prodCongr, MeasureTheory.addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv, NumberField.AdeleRing.DivisionAlgebra.Aux.D𝔸ProdRight'' and 16 more
129 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
def NumberField.AdeleRing.DivisionAlgebra.Aux.Uf An auxiliary compact subset of D_𝔸^f with nonempty interior line 674 source
Source documentation
An auxiliary compact subset of D_𝔸^f with nonempty interior
```
def Uf : Set (D ⊗[K] (FiniteAdeleRing (𝓞 K) K)) := (exists_compact_mem_nhds 0).choose
```
theorem NumberField.AdeleRing.DivisionAlgebra.Aux.Uf.spec line 676 source
def NumberField.AdeleRing.DivisionAlgebra.Aux.Ui An auxiliary compact subset of D_∞ with nonempty interior line 679 source
Source documentation
An auxiliary compact subset of D_∞ with nonempty interior
```
def Ui : Set (D ⊗[K] (InfiniteAdeleRing K)) := (exists_compact_mem_nhds 0).choose
```
theorem NumberField.AdeleRing.DivisionAlgebra.Aux.Ui.spec line 681 source
def NumberField.AdeleRing.DivisionAlgebra.Aux.Efamily Documented declaration: Efamily line 693 source
Source documentation
An auxiliary definition of an increasing family of compact subsets of D_𝔸, defined as the product of a compact neighbourhood of 0 at the finite places and a compact neighbourhood of 0, scaled by r, at the infinite places.
```
def Efamily (r : ℝ) : Set (D_𝔸) :=
…
```
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.E_family_compact line 696 source
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.E_family_nonempty_interior line 701 source
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.E_family_unbounded line 711 source
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.existsE line 774 source
def NumberField.AdeleRing.DivisionAlgebra.Aux.E An auxiliary set E used in the proof of Fujisaki's lemma line 798 source
Source documentation
An auxiliary set E used in the proof of Fujisaki's lemma.
```
def E : Set D_𝔸 := (existsE K D).choose
```
Mentions: NumberField.AdeleRing.DivisionAlgebra.Aux.existsE
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.E_compact line 800 source
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.E_noninjective_left line 802 source
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.E_noninjective_right line 807 source
depends on sorry (Lean reported 10 error(s) in this file) what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, FiniteDimensional, Algebra.IsCentral, Units, TensorProduct, NumberField.AdeleRing, NumberField.RingOfIntegers, Membership.mem, Subgroup, MeasureTheory.ringHaarCharKer, TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT, TensorProduct.RightActions.instIsTopologicalRing_fLT_1, TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT, Exists, And, Set, NumberField.AdeleRing.DivisionAlgebra.Aux.E and 7 more
Proof uses: ContinuousAddEquiv, ContinuousAddEquiv.mulRight, Eq, NNReal, MeasureTheory.addEquivAddHaarChar, TensorProduct.RightActions.instIsTopologicalAddGroup_fLT, OfNat.ofNat, Eq.mp, ContinuousAddEquiv.mulLeft, congrArg, NumberField.AdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul, ContinuousMonoidHom, MeasureTheory.ringHaarChar, MeasureTheory.ringHaarChar_apply, propext, MeasureTheory.mem_ringHaarChar_ker, Eq.symm, inv_mem_iff, And.right, IsCompact and 3 more
117 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def NumberField.AdeleRing.DivisionAlgebra.Aux.X An auxiliary set X used in the proof of Fukisaki's lemma line 818 source
Source documentation
An auxiliary set X used in the proof of Fukisaki's lemma. Defined as E - E.
```
def X : Set D_𝔸 := E K D - E K D
…
```
Mentions: NumberField.AdeleRing.DivisionAlgebra.Aux.E
def NumberField.AdeleRing.DivisionAlgebra.Aux.Y An auxiliary set Y used in the proof of Fukisaki's lemma line 822 source
Source documentation
An auxiliary set Y used in the proof of Fukisaki's lemma. Defined as X * X.
```
def Y : Set D_𝔸 := X K D * X K D
```
Mentions: NumberField.AdeleRing.DivisionAlgebra.Aux.X
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.X_compact line 824 source
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.Y_compact line 829 source
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel line 833 source
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel' line 846 source
depends on sorry (Lean reported 10 error(s) in this file) what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, FiniteDimensional, Algebra.IsCentral, Units, TensorProduct, NumberField.AdeleRing, NumberField.RingOfIntegers, Membership.mem, Subgroup, MeasureTheory.ringHaarCharKer, TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT, TensorProduct.RightActions.instIsTopologicalRing_fLT_1, TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT, Exists, And, Set, NumberField.AdeleRing.DivisionAlgebra.Aux.X and 6 more
Proof uses: NumberField.AdeleRing.DivisionAlgebra.Aux.E, Ne, AlgHom, Algebra.TensorProduct.includeLeft, HSub.hSub, NumberField.AdeleRing.DivisionAlgebra.Aux.E_noninjective_right, Exists.intro, And.intro, Set.sub_mem_sub, IsUnit, OfNat.ofNat, Eq.mpr, Not, id, congrArg, sub_ne_zero_of_ne, TensorProduct.tmul, False, False.elim, Eq.mp and 11 more
126 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
def NumberField.AdeleRing.DivisionAlgebra.Aux.T An auxiliary set T used in the proof of Fukisaki's lemma line 860 source
Source documentation
An auxiliary set T used in the proof of Fukisaki's lemma. Defined as Y ∩ Dˣ.
```
def T : Set D_𝔸ˣ := ((↑) : D_𝔸ˣ → D_𝔸) ⁻¹' (Y K D) ∩ Set.range ((incl K D : Dˣ → D_𝔸ˣ))
```
Mentions: NumberField.AdeleRing.DivisionAlgebra.Aux.Y, NumberField.AdeleRing.DivisionAlgebra.Aux.incl
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.T_finite_extracted1 line 862 source
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.T_finite line 870 source
def NumberField.AdeleRing.DivisionAlgebra.Aux.C An auxiliary set C used in the proof of Fukisaki's lemma line 882 source
Source documentation
An auxiliary set C used in the proof of Fukisaki's lemma. Defined as T⁻¹X × X.
```
def C : Set (D_𝔸 × D_𝔸) := ((((↑) : D_𝔸ˣ → D_𝔸) '' (T K D)⁻¹) * X K D) ×ˢ X K D
```
Mentions: NumberField.AdeleRing.DivisionAlgebra.Aux.T, NumberField.AdeleRing.DivisionAlgebra.Aux.X
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.C_compact line 884 source
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.antidiag_mem_C line 892 source
depends on sorry (Lean reported 10 error(s) in this file) what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, FiniteDimensional, Algebra.IsCentral, Units, TensorProduct, NumberField.AdeleRing, NumberField.RingOfIntegers, Membership.mem, Subgroup, MeasureTheory.ringHaarCharKer, TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT, TensorProduct.RightActions.instIsTopologicalRing_fLT_1, TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT, Exists, And, Set, Set.range and 8 more
Proof uses: NumberField.AdeleRing.DivisionAlgebra.Aux.X, NumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel, NumberField.AdeleRing.DivisionAlgebra.Aux.X_meets_kernel', IsUnit, Exists.intro, Eq.symm, Iff.mpr, Units.eq_inv_mul_iff_mul_eq, Iff.mp, Units.mul_inv_eq_iff_eq_mul, NumberField.AdeleRing.DivisionAlgebra.Aux.T, And.intro, Set.preimage, NumberField.AdeleRing.DivisionAlgebra.Aux.Y, id, Set.mul_mem_mul, Eq.mpr, congrArg, map_mul, Eq.mp and 28 more
126 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
def NumberField.AdeleRing.DivisionAlgebra.Aux.incl₂ The inclusion of ringHaarCharKer D_𝔸 into the product space D_𝔸 × D_𝔸ᵐᵒᵖ line 914 source
Source documentation
The inclusion of ringHaarCharKer D_𝔸 into the product space D_𝔸 × D_𝔸ᵐᵒᵖ.
```
def incl₂ : ringHaarCharKer D_𝔸 → Prod D_𝔸 D_𝔸ᵐᵒᵖ :=
…
```
def NumberField.AdeleRing.DivisionAlgebra.Aux.M An auxiliary set used in the proof of compact_quotient' line 918 source
Source documentation
An auxiliary set used in the proof of compact_quotient'.
```
def M : Set (ringHaarCharKer D_𝔸) := Set.preimage (incl₂ K D)
…
```
Mentions: NumberField.AdeleRing.DivisionAlgebra.Aux.incl₂
abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.toQuot The map from ringHaarCharKer D_𝔸 to the quotient Dˣ \ ringHaarCharKer D_𝔸 line 922 source
Source documentation
The map from ringHaarCharKer D_𝔸 to the quotient Dˣ \ ringHaarCharKer D_𝔸.
```
abbrev toQuot (a : ringHaarCharKer D_𝔸) : (_root_.Quotient (QuotientGroup.rightRel
    ((MonoidHom.range (incl K D)).comap (ringHaarCharKer D_𝔸).subtype))) :=
…
```
Mentions: NumberField.AdeleRing.DivisionAlgebra.Aux.incl
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.toQuot_cont line 927 source
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.toQuot_surjective line 931 source
depends on sorry (Lean reported 10 error(s) in this file) what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, FiniteDimensional, Algebra.IsCentral, Eq, Set, Quotient, Subtype, Units, TensorProduct, NumberField.AdeleRing, NumberField.RingOfIntegers, Membership.mem, Subgroup, MeasureTheory.ringHaarCharKer, TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT, TensorProduct.RightActions.instIsTopologicalRing_fLT_1, TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT and 9 more
Proof uses: Eq.mpr, id, congrArg, propext, Set.eq_univ_iff_forall, Quot.ind, Quot.mk, And, Set.range, MonoidHom, Exists, HMul.hMul, Prod, NumberField.AdeleRing.DivisionAlgebra.Aux.C, Prod.mk, Inv.inv, Subtype.mk, NumberField.AdeleRing.DivisionAlgebra.Aux.antidiag_mem_C, Subgroup.subgroupOf, Quotient.mk and 21 more
94 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.incl₂_isClosedEmbedding line 953 source
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.ImAux_isCompact line 964 source
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.M_compact line 967 source
abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.rest₁ The restriction of ringHaarCharKer D_𝔸 to (D ⊗ 𝔸_K^∞)ˣ via D𝔸_iso_prod_units line 971 source
Source documentation
The restriction of ringHaarCharKer D_𝔸 to (D ⊗ 𝔸_K^∞)ˣ via D𝔸_iso_prod_units.
```
abbrev rest₁ : ringHaarCharKer D_𝔸 → Dfx K D :=
…
```
Mentions: NumberField.AdeleRing.DivisionAlgebra.Aux.Dfx
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.rest₁_continuous line 974 source
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.ringHaarChar_D𝔸_prodRight_units_aux line 978 source
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.rest₁_surjective line 984 source
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.incl_D𝔸quot_equivariant the goal that comes up when you define the map Dˣ \ D_𝔸^(1) to Dˣ \ (Dfx K D) below using Quot.lift line 1007 source
Source comment
the goal that comes up when you define the map `Dˣ \ D_𝔸^(1) to Dˣ \ (Dfx K D)` below using Quot.lift
```
lemma incl_D𝔸quot_equivariant : ∀ (a b : ↥(ringHaarCharKer D_𝔸)),
    (QuotientGroup.rightRel (Subgroup.comap (ringHaarCharKer D_𝔸).subtype
    (AdeleRing.DivisionAlgebra.Aux.incl K D).range)) a b →
    (Quotient.mk (QuotientGroup.rightRel (incl₁ K D).range) (rest₁ K D a) =
     Quotient.mk (QuotientGroup.rightRel (incl₁ K D).range) (rest₁ K D b)) := by
…
```
Mentions: NumberField.AdeleRing.DivisionAlgebra.Aux.incl, NumberField.AdeleRing.DivisionAlgebra.Aux.incl₁, NumberField.AdeleRing.DivisionAlgebra.Aux.rest₁
abbrev NumberField.AdeleRing.DivisionAlgebra.Aux.inclD𝔸quot The obvious map Dˣ \ D_𝔸^(1) to Dˣ \ (Dfx K D) line 1025 source
Source documentation
The obvious map Dˣ \ D_𝔸^(1) to Dˣ \ (Dfx K D).
```
abbrev inclD𝔸quot : Quotient (QuotientGroup.rightRel
    ((MonoidHom.range (NumberField.AdeleRing.DivisionAlgebra.Aux.incl K D)).comap
    (ringHaarCharKer D_𝔸).subtype)) →
    Quotient (QuotientGroup.rightRel (incl₁ K D).range) :=
…
```
Mentions: NumberField.AdeleRing.DivisionAlgebra.Aux.incl, NumberField.AdeleRing.DivisionAlgebra.Aux.incl₁
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.incl_D𝔸quot_continuous line 1033 source
lemma NumberField.AdeleRing.DivisionAlgebra.Aux.incl_D𝔸quot_surjective line 1037 source
lemma NumberField.AdeleRing.DivisionAlgebra.compact_quotient Dˣ \ D_𝔸^{(1)} is compact line 1057 source
Source documentation
Dˣ \ D_𝔸^{(1)} is compact.

depends on sorry (Lean reported 10 error(s) in this file) what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, FiniteDimensional, Algebra.IsCentral, CompactSpace, Quotient, Subtype, Units, TensorProduct, NumberField.AdeleRing, NumberField.RingOfIntegers, Membership.mem, Subgroup, MeasureTheory.ringHaarCharKer, TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT, TensorProduct.RightActions.instIsTopologicalRing_fLT_1, TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT, QuotientGroup.rightRel and 4 more
Proof uses: Iff.mp, IsCompact, Set.univ, isCompact_univ_iff, Eq.mp, Set.image, NumberField.AdeleRing.DivisionAlgebra.Aux.toQuot, NumberField.AdeleRing.DivisionAlgebra.Aux.M, congrArg, Set, NumberField.AdeleRing.DivisionAlgebra.Aux.toQuot_surjective, IsCompact.image, NumberField.AdeleRing.DivisionAlgebra.Aux.M_compact, NumberField.AdeleRing.DivisionAlgebra.Aux.toQuot_cont
64 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma compact_quotient [Algebra.IsCentral K D] :
    CompactSpace (_root_.Quotient (QuotientGroup.rightRel
    ((MonoidHom.range (incl K D)).comap (ringHaarCharKer D_𝔸).subtype))) :=
…
```
theorem NumberField.AdeleRing.DivisionAlgebra._root_.NumberField.FiniteAdeleRing.DivisionAlgebra.units_cocompact Dˣ \ D_𝔸^fˣ is compact line 1066 source
Source documentation
Dˣ \ D_𝔸^fˣ is compact.
```
theorem _root_.NumberField.FiniteAdeleRing.DivisionAlgebra.units_cocompact :
    CompactSpace (_root_.Quotient (QuotientGroup.rightRel (incl₁ K D).range)) := by
…
```
theorem NumberField.AdeleRing.DivisionAlgebra._root_.NumberField.FiniteAdeleRing.DivisionAlgebra.finiteDoubleCoset line 1081 source