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

69 declarations, 0 contain sorry, 0 declared as axioms

Definitions of various compact open subgrups of Dˣ and GL₂(𝔸_F^∞)

We define U₁(v) as a subgroup of GL₂(Fᵥ), and U₁(S) as a subgroup of GL₂(𝔸_F^∞). We introduce the concept of a rigidification r : (D ⊗[F] 𝔸_F^∞) ≅ M₂(𝔸_F^∞) in order to push U₁(S) over to a subgroup of (D ⊗[F] 𝔸_F^∞)ˣ.

Imports (14)

Imported by 3 files

class IsQuaternionAlgebra.NumberField.WithRigidification A rigidification of a quaternion algebra D over a number field F is a fixed choice of 𝔸_F^∞-algebra isomorphism D ⊗[F] 𝔸_F^∞ = M₂(𝔸_F^∞) line 67 source
Source documentation
A rigidification of a quaternion algebra D over a number field F is a fixed choice of 𝔸_F^∞-algebra isomorphism D ⊗[F] 𝔸_F^∞ = M₂(𝔸_F^∞). In other words, it is a choice of splitting of D ⊗[F] Fᵥ (i.e. an isomorphism to M₂(Fᵥ)) for all finite places v together with a guarantee that the isomorphism works on the integral level at all but finitely many places. Such a rigidification exists if and only if F is unramified at all finite places.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra
3 instances, coercions and auxiliary constants left out.
```
class WithRigidification where
…
```
def IsQuaternionAlgebra.NumberField.WithRigidification.algEquiv Given a rigidification of D, D ⊗ 𝔸ᶠ is isomorphic to M₂(𝔸ᶠ) line 80 source
Source documentation
Given a rigidification of D, D ⊗ 𝔸ᶠ is isomorphic to M₂(𝔸ᶠ).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, AlgEquiv, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, TensorProduct, Matrix, Fin, OfNat.ofNat, Nat, TensorProduct.RightActions.instAlgebra_fLT
Proof uses: AlgEquiv.trans, Algebra.TensorProduct.comm, AlgEquiv.mk, AlgEquiv.toEquiv, AlgEquiv.ofBijective, Algebra.TensorProduct.lift, Algebra.ofId, IsQuaternionAlgebra.NumberField.WithRigidification.incl, IsQuaternionAlgebra.NumberField.WithRigidification.cond
49 instances, coercions and auxiliary constants left out.
```
noncomputable def WithRigidification.algEquiv :
    D ⊗[F] 𝔸ᶠ[F] ≃ₐ[𝔸ᶠ[F]] M₂(𝔸ᶠ[F]) :=
…
```
lemma IsQuaternionAlgebra.NumberField.WithRigidification.algEquiv_tmul line 88 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Eq, Matrix, Fin, OfNat.ofNat, Nat, AlgEquiv, TensorProduct, TensorProduct.RightActions.instAlgebra_fLT, IsQuaternionAlgebra.NumberField.WithRigidification.algEquiv, TensorProduct.tmul, HSMul.hSMul, AlgHom, IsQuaternionAlgebra.NumberField.WithRigidification.incl
Proof uses: of_eq_true, HMul.hMul, RingHom, Algebra.algebraMap, Eq.trans, True, congrArg, Algebra.smul_def, eq_self
55 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
abbrev IsQuaternionAlgebra.NumberField.WithRigidification.unitsIncl Given a rigidification, we get an embedding Dˣ ↪ GL₂(𝔸_F) line 93 source
Source documentation
Given a rigidification, we get an embedding Dˣ ↪ GL₂(𝔸_F).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, MonoidHom, Units, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Matrix
Proof uses: Units.map, AlgHom.toRingHom, IsQuaternionAlgebra.NumberField.WithRigidification.incl
36 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev WithRigidification.unitsIncl : Dˣ →* GL₂(𝔸ᶠ[F]) :=
…
```
instance IsQuaternionAlgebra.NumberField.(instance at line 97) line 97 source
lemma IsQuaternionAlgebra.NumberField.WithRigidification.smul_def line 101 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, Matrix, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Eq, HSMul.hSMul, HMul.hMul, AlgHom, IsQuaternionAlgebra.NumberField.WithRigidification.incl
Proof uses: rfl
67 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
instance IsQuaternionAlgebra.NumberField.(instance at line 103) line 103 source
instance IsQuaternionAlgebra.NumberField.(instance at line 106) line 106 source
instance IsQuaternionAlgebra.NumberField.(instance at line 109) line 109 source
lemma IsQuaternionAlgebra.NumberField.HeightOneSpectrum.nonempty line 112 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Not, IsField, Nontrivial, Nonempty, IsDedekindDomain.HeightOneSpectrum
Proof uses: Ideal, Ideal.IsMaximal, Exists, Ideal.exists_maximal, Nonempty.intro, IsDedekindDomain.HeightOneSpectrum.mk, inferInstance, Ideal.IsPrime, Eq, Bot.bot, False, Iff.mpr, Ring.isField_iff_maximal_bot, Eq.symm
10 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma IsQuaternionAlgebra.NumberField.WithRigidification.incl_injective line 118 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, Function.Injective, Matrix, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, AlgHom, IsQuaternionAlgebra.NumberField.WithRigidification.incl
Proof uses: Function.Injective.of_comp, TensorProduct, AlgEquiv, TensorProduct.RightActions.instAlgebra_fLT, AlgEquiv.symm, IsQuaternionAlgebra.NumberField.WithRigidification.algEquiv, Eq.mpr, Function.comp, Algebra.TensorProduct.includeLeft, eq_of_heq, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, funext, AlgEquiv.injective, of_eq_true, Eq.trans, True and 11 more
82 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma IsQuaternionAlgebra.NumberField.WithRigidification.unitsIncl_injective line 127 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, Function.Injective, Units, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, MonoidHom, Matrix, IsQuaternionAlgebra.NumberField.WithRigidification.unitsIncl
Proof uses: Units.map_injective, AlgHom.toRingHom, IsQuaternionAlgebra.NumberField.WithRigidification.incl, IsQuaternionAlgebra.NumberField.WithRigidification.incl_injective
38 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma IsQuaternionAlgebra.NumberField.WithRigidification.det_incl_sq line 134 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, Module.Finite, Eq, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, HPow.hPow, Nat, Matrix.det, Fin, OfNat.ofNat, AlgHom, Matrix, IsQuaternionAlgebra.NumberField.WithRigidification.incl, RingHom, Algebra.algebraMap, MonoidHom and 1 more
Proof uses: TensorProduct, TensorProduct.tmul, Algebra.norm_one_tmul, Eq.mp, HMul.hMul, Fintype.card, congrFun', congrArg, Eq.trans, map_one, one_mul, Algebra.norm_eq_det, AlgEquiv, AlgEquiv.ofBijective, Algebra.TensorProduct.lift, Algebra.ofId, Algebra.commute_algebraMap_left, IsQuaternionAlgebra.NumberField.WithRigidification.cond, Eq.symm, Algebra.norm_eq_of_algEquiv
102 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma IsQuaternionAlgebra.NumberField.WithRigidification.unitsIncl_algebraMap line 146 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, Units, Eq, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, MonoidHom, Matrix, IsQuaternionAlgebra.NumberField.WithRigidification.unitsIncl, Units.map, Algebra.algebraMap
Proof uses: Units.ext, of_eq_true, RingHom, Eq.trans, True, congrFun', congrArg, AlgHom.commutes, IsQuaternionAlgebra.NumberField.WithRigidification.incl, eq_self
48 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
abbrev IsQuaternionAlgebra.NumberField.IsUnramified A quaternion algebra over a number field is unramified if it is split at all finite places line 159 source
Source documentation
A quaternion algebra over a number field is unramified if it is split at all finite places. This is implemented as the existence of a rigidification of D, that is, an isomorphism D ⊗[F] 𝔸_F^∞ = M₂(𝔸_F^∞).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra
Proof uses: Nonempty, IsQuaternionAlgebra.NumberField.WithRigidification
6 instances, coercions and auxiliary constants left out.
```
abbrev IsUnramified : Prop := Nonempty (WithRigidification F D)
…
```
Mentions: IsQuaternionAlgebra.NumberField.WithRigidification
def IsDedekindDomain.M2.localFullLevel M_2(O_v) as a subring of M_2(F_v) line 172 source
Source documentation
M_2(O_v) as a subring of M_2(F_v).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Subring, Matrix, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion
Proof uses: Subring.matrix, ValuationSubring.toSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers
23 instances, coercions and auxiliary constants left out.
```
noncomputable def M2.localFullLevel (v : HeightOneSpectrum (𝓞 F)) :
    Subring M₂(v.adicCompletion F) :=
…
```
def IsDedekindDomain.GL2.localFullLevel GL₂(𝒪ᵥ) as a subgroup of GL₂(Fᵥ) line 177 source
Source documentation
GL₂(𝒪ᵥ) as a subgroup of GL₂(Fᵥ).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Subgroup, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Matrix
Proof uses: MonoidHom.range, Units, Subtype, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Units.map, RingHom.mapMatrix, ValuationSubring.subtype
35 instances, coercions and auxiliary constants left out.
```
noncomputable def GL2.localFullLevel (v : HeightOneSpectrum (𝓞 F)) :
    Subgroup GL₂(v.adicCompletion F) :=
…
```
theorem IsDedekindDomain.M2.localFullLevel.isOpen line 182 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, IsOpen, Matrix, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Subring, IsDedekindDomain.M2.localFullLevel
Proof uses: IsOpen.matrix, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, NumberField.isOpenAdicCompletionIntegers
29 instances, coercions and auxiliary constants left out.
theorem IsDedekindDomain.M2.localFullLevel.isCompact line 186 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, IsCompact, Matrix, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Subring, IsDedekindDomain.M2.localFullLevel
Proof uses: IsCompact.matrix, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Iff.mpr, CompactSpace, Membership.mem, Set, isCompact_iff_compactSpace
31 instances, coercions and auxiliary constants left out.
lemma IsDedekindDomain.M2.units_localFullLevel line 191 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Eq, Subgroup, Units, Matrix, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Submonoid.units, Subsemiring.toSubmonoid, Subring.toSubsemiring, IsDedekindDomain.M2.localFullLevel, IsDedekindDomain.GL2.localFullLevel
Proof uses: Eq.mpr, MonoidHom.range, Subtype, Membership.mem, Submonoid, Subring.matrix, ValuationSubring.toSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Units.map, Submonoid.subtype, ValuationSubring, Matrix.GeneralLinearGroup, RingHom.mapMatrix, ValuationSubring.subtype, id, congrFun', congrArg, Subring, MonoidHom.comp, MulEquiv and 6 more
76 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem IsDedekindDomain.GL2.localFullLevel.isOpen the clever way to prove this is a theorem of the form "if A is an open submonoid of R then Aˣ is an open subgroup of Rˣ" line 201 source
Source comment
the clever way to prove this is a theorem of the form "if A is an open submonoid of R then Aˣ is an open subgroup of Rˣ"

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, IsOpen, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Matrix, Subgroup, IsDedekindDomain.GL2.localFullLevel
Proof uses: Eq.rec, Units, Submonoid.units, Subsemiring.toSubmonoid, Subring.toSubsemiring, IsDedekindDomain.M2.localFullLevel, Eq, Submonoid.isOpen_units, IsDedekindDomain.M2.localFullLevel.isOpen, IsDedekindDomain.M2.units_localFullLevel
45 instances, coercions and auxiliary constants left out.
```
theorem GL2.localFullLevel.isOpen (v : HeightOneSpectrum (𝓞 F)) :
    IsOpen (X := GL₂(v.adicCompletion F)) (GL2.localFullLevel v) :=
…
```
Mentions: IsDedekindDomain.GL2.localFullLevel
theorem IsDedekindDomain.GL2.localFullLevel.isCompact the clever way to prove this is a theorem of the form "if A is a compact submonoid of R then Aˣ is a compact subgroup of Rˣ" line 207 source
Source comment
the clever way to prove this is a theorem of the form "if A is a compact submonoid of R then Aˣ is a compact subgroup of Rˣ"

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, IsCompact, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Matrix, Subgroup, IsDedekindDomain.GL2.localFullLevel
Proof uses: Eq.rec, Units, Submonoid.units, Subsemiring.toSubmonoid, Subring.toSubsemiring, IsDedekindDomain.M2.localFullLevel, Eq, Submonoid.units_isCompact, WithZero, Multiplicative, Int, IsDedekindDomain.M2.localFullLevel.isCompact, IsDedekindDomain.M2.units_localFullLevel
79 instances, coercions and auxiliary constants left out.
```
theorem GL2.localFullLevel.isCompact (v : HeightOneSpectrum (𝓞 F)) :
    IsCompact (X := GL₂(v.adicCompletion F)) (GL2.localFullLevel v) :=
…
```
Mentions: IsDedekindDomain.GL2.localFullLevel
lemma IsDedekindDomain.GL2.mem_localFullLevel line 211 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, Subgroup, Matrix, IsDedekindDomain.GL2.localFullLevel, Exists, Subtype, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Eq, Units, MonoidHom and 3 more
46 instances, coercions and auxiliary constants left out.
lemma IsDedekindDomain.GL2.mem_localFullLevel' line 217 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, Subgroup, Matrix, IsDedekindDomain.GL2.localFullLevel, Exists, Subtype, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Eq
Proof uses: Exists.imp, Units, MonoidHom, Units.map, RingHom.mapMatrix, ValuationSubring.subtype, Eq.mpr, Matrix.map, RingHom, id, forall_congr, implies_congr, Eq.trans, congrFun', congrArg, RingHom.mapMatrix_apply, Eq.refl, of_eq_true, True, Eq.symm and 3 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
instance IsDedekindDomain.(instance at line 228) line 228 source
instance IsDedekindDomain.(instance at line 230) line 230 source
lemma IsDedekindDomain.GL2.v_det_val_mem_localFullLevel_eq_one line 233 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, Subgroup, Matrix, IsDedekindDomain.GL2.localFullLevel, Eq, WithZero, Multiplicative, Int, Valuation, Valued.v, Matrix.det
Proof uses: Subtype, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Units, MonoidHom, Units.map, RingHom.mapMatrix, ValuationSubring.subtype, Exists, IsDedekindDomain.GL2.mem_localFullLevel, IsUnit, Matrix.GeneralLinearGroup.det, of_eq_true, Eq.trans, True, congrArg, Matrix.GeneralLinearGroup.val_det_apply, Eq.mpr, HSub.hSub, HMul.hMul and 12 more
110 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma IsDedekindDomain.GL2.v_le_one_of_mem_localFullLevel line 242 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, Subgroup, Matrix, IsDedekindDomain.GL2.localFullLevel, LE.le, WithZero, Multiplicative, Int, Valuation, Valued.v
Proof uses: Units, Subtype, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Eq, Subring, ValuationSubring.toSubring, Exists, Eq.mp, Eq.trans, MonoidHom, MonoidHom.mk', Units.mk, Equiv, Matrix.of, Inv.inv, RingHom.mapMatrix, ValuationSubring.subtype, HMul.hMul, Units.inv and 21 more
108 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma IsDedekindDomain.GL2.mem_localFullLevel_iff_v line 252 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Iff, Membership.mem, Subgroup, Matrix, IsDedekindDomain.GL2.localFullLevel, And, LE.le, WithZero, Multiplicative, Int, Valuation and 3 more
Proof uses: Iff.intro, And.intro, IsDedekindDomain.GL2.v_le_one_of_mem_localFullLevel, IsDedekindDomain.GL2.v_det_val_mem_localFullLevel_eq_one, Subtype, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Equiv, Matrix.of, Subtype.mk, Eq.mpr, HSub.hSub, HMul.hMul, id, congrArg, Matrix.det_fin_two, of_eq_true, eq_self, IsUnit, Valuation.valuationSubring and 41 more
122 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
def IsDedekindDomain.GL2.localIwahoriLevel local U₀(v), defined as a subgroup of GL₂(Fᵥ) given by matrices in GL₂(𝒪ᵥ) congruent to (* *;0 *) mod v line 271 source
Source documentation
local U₀(v), defined as a subgroup of GL₂(Fᵥ) given by matrices in GL₂(𝒪ᵥ) congruent to (* *;0 *) mod v.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Subgroup, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Matrix
Proof uses: Subgroup.mk, Submonoid.mk, Subsemigroup.mk, Set.ofPred, And, Membership.mem, IsDedekindDomain.GL2.localFullLevel, LT.lt, WithZero, Multiplicative, Int, Valuation, Valued.v, Set
59 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
noncomputable def GL2.localIwahoriLevel (v : HeightOneSpectrum (𝓞 F)) :
    Subgroup (GL (Fin 2) (v.adicCompletion F)) where
…
```
lemma IsDedekindDomain.GL2.mem_localIwahoriLevel line 290 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Iff, Membership.mem, Subgroup, Matrix, IsDedekindDomain.GL2.localIwahoriLevel, And, IsDedekindDomain.GL2.localFullLevel, LT.lt, WithZero, Multiplicative, Int and 2 more
Proof uses: Iff.rfl
52 instances, coercions and auxiliary constants left out.
lemma IsDedekindDomain.GL2.mem_localIwahoriLevel_iff_v line 293 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Iff, Membership.mem, Subgroup, Matrix, IsDedekindDomain.GL2.localIwahoriLevel, And, Eq, WithZero, Multiplicative, Int, Valuation and 3 more
Proof uses: Trans.simple, Matrix.det, Eq.mpr, id, congrFun', congrArg, Eq.trans, IsDedekindDomain.GL2.localFullLevel, forall_congr, congr, implies_congr, Eq.refl, HMul.hMul, HSub.hSub, Matrix.det_fin_two, Iff.intro, HAdd.hAdd, Eq.symm, sub_add_cancel, Valuation.map_add_eq_of_lt_left and 23 more
185 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
theorem IsDedekindDomain.GL2.localIwahoriLevel.isOpen the clever way to prove this is a theorem of the form "if A is an open submonoid of R then Aˣ is an open subgroup of Rˣ" line 324 source
Source comment
the clever way to prove this is a theorem of the form "if A is an open submonoid of R then Aˣ is an open subgroup of Rˣ"

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, IsOpen, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Matrix, Subgroup, IsDedekindDomain.GL2.localIwahoriLevel
Proof uses: Eq.mpr, Inter.inter, Set, IsDedekindDomain.GL2.localFullLevel, Set.preimage, Units, Set.ofPred, LT.lt, MonoidWithZeroHom.ValueGroup₀, WithZero, Multiplicative, Int, Valued.v, Subtype, Membership.mem, MonoidWithZeroHom.valueGroup, Valuation, Valuation.restrict, eq_of_heq, TopologicalSpace and 16 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem GL2.localIwahoriLevel.isOpen (v : HeightOneSpectrum (𝓞 F)) :
    IsOpen (X := GL₂(v.adicCompletion F)) (GL2.localIwahoriLevel v) := by
…
```
Mentions: IsDedekindDomain.GL2.localIwahoriLevel
theorem IsDedekindDomain.GL2.localIwahoriLevel.isCompact the clever way to prove this is a theorem of the form "if A is a compact submonoid of R then Aˣ is a compact subgroup of Rˣ" line 333 source
Source comment
the clever way to prove this is a theorem of the form "if A is a compact submonoid of R then Aˣ is a compact subgroup of Rˣ"

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, IsCompact, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Matrix, Subgroup, IsDedekindDomain.GL2.localIwahoriLevel
Proof uses: Eq.mpr, Inter.inter, Set, IsDedekindDomain.GL2.localFullLevel, Set.preimage, Units, Set.ofPred, LT.lt, MonoidWithZeroHom.ValueGroup₀, WithZero, Multiplicative, Int, Valued.v, Subtype, Membership.mem, MonoidWithZeroHom.valueGroup, Valuation, Valuation.restrict, eq_of_heq, TopologicalSpace and 16 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem GL2.localIwahoriLevel.isCompact (v : HeightOneSpectrum (𝓞 F)) :
    IsCompact (X := GL₂(v.adicCompletion F)) (GL2.localIwahoriLevel v) := by
…
```
Mentions: IsDedekindDomain.GL2.localIwahoriLevel
def IsDedekindDomain.GL2.localFullLevelEquiv line 344 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, MulEquiv, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, Subgroup, Matrix, IsDedekindDomain.GL2.localFullLevel, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers
Proof uses: MulEquiv.symm, MulEquiv.ofBijective, MonoidHom, Units, MonoidHom.range, Units.map, RingHom.mapMatrix, ValuationSubring.subtype, MonoidHom.rangeRestrict
59 instances, coercions and auxiliary constants left out.
lemma IsDedekindDomain.GL2.localFullLevelEquiv_symm_apply line 353 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Eq, Subgroup, Matrix, IsDedekindDomain.GL2.localFullLevel, MulEquiv, MulEquiv.symm, IsDedekindDomain.GL2.localFullLevelEquiv and 3 more
Proof uses: rfl
63 instances, coercions and auxiliary constants left out.
lemma IsDedekindDomain.GL2.localFullLevelEquiv_apply line 358 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, Subgroup, Matrix, IsDedekindDomain.GL2.localFullLevel, Eq, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, MulEquiv, IsDedekindDomain.GL2.localFullLevelEquiv
Proof uses: Equiv, Matrix.of, Subtype.mk, IsDedekindDomain.GL2.v_le_one_of_mem_localFullLevel, Subtype.property, Matrix.map_injective, Subtype.val_injective, id, Matrix.map, Eq.mpr, MulEquiv.symm, congrFun', congrArg, MulEquiv.symm_apply_apply, Matrix.ext, of_eq_true, eq_self, Eq.trans, True
61 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma IsDedekindDomain.GL2.localIwahoriLevel_le_localFullLevel line 368 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, LE.le, Subgroup, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Matrix, IsDedekindDomain.GL2.localIwahoriLevel, IsDedekindDomain.GL2.localFullLevel
Proof uses: Membership.mem, And.left, LT.lt, WithZero, Multiplicative, Int, Valuation, Valued.v
53 instances, coercions and auxiliary constants left out.
def IsDedekindDomain.GL2.localIwahoriLevel.char line 376 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, MonoidHom, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, Subgroup, Matrix, IsDedekindDomain.GL2.localIwahoriLevel, Units, IsLocalRing.ResidueField, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers
Proof uses: MonoidHom.toHomUnits, MonoidHom.mk, OneHom.mk, HDiv.hDiv, RingHom, IsLocalRing.residue, MulEquiv, IsDedekindDomain.GL2.localFullLevel, IsDedekindDomain.GL2.localFullLevelEquiv, Subgroup.inclusion, IsDedekindDomain.GL2.localIwahoriLevel_le_localFullLevel
74 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma IsDedekindDomain.GL2.v_zero_zero_eq_one_of_mem_localIwahoriLevel line 391 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, Subgroup, Matrix, IsDedekindDomain.GL2.localIwahoriLevel, Eq, WithZero, Multiplicative, Int, Valuation, Valued.v
Proof uses: Ne, IsLocalRing.ResidueField, Subtype, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, MonoidHom, Units, IsDedekindDomain.GL2.localIwahoriLevel.char, Subtype.mk, Units.ne_zero, of_eq_true, Eq.trans, True, congrFun', congrArg, And, id, Eq.mp, Not, HDiv.hDiv and 15 more
122 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma IsDedekindDomain.GL2.v_one_one_eq_one_of_mem_localIwahoriLevel line 398 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, Subgroup, Matrix, IsDedekindDomain.GL2.localIwahoriLevel, Eq, WithZero, Multiplicative, Int, Valuation, Valued.v
Proof uses: Ne, IsLocalRing.ResidueField, Subtype, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, MonoidHom, Units, IsDedekindDomain.GL2.localIwahoriLevel.char, Subtype.mk, Units.ne_zero, of_eq_true, Eq.trans, True, congrFun', congrArg, And, id, Eq.mp, Not, HDiv.hDiv and 15 more
122 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma IsDedekindDomain.GL2.localIwahoriLevel.char_eq_one_iff line 405 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, Subgroup, Matrix, IsDedekindDomain.GL2.localIwahoriLevel, Iff, Eq, Units, IsLocalRing.ResidueField, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers and 9 more
Proof uses: Eq.mpr, HDiv.hDiv, RingHom, IsLocalRing.residue, MulEquiv, IsDedekindDomain.GL2.localFullLevel, IsDedekindDomain.GL2.localFullLevelEquiv, Subgroup.inclusion, IsDedekindDomain.GL2.localIwahoriLevel_le_localFullLevel, id, congrFun', congrArg, MonoidHom.toHomUnits, MonoidHom.mk, OneHom.mk, propext, div_eq_one_iff_eq, of_eq_true, Not, Eq.trans and 22 more
179 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
def IsDedekindDomain.GL2.localTameLevel local U_1(v), defined as a subgroup of GL₂(Fᵥ) given by matrices in GL₂(𝒪ᵥ) congruent to (a *;0 a) mod v line 419 source
Source documentation
local U_1(v), defined as a subgroup of GL₂(Fᵥ) given by matrices in GL₂(𝒪ᵥ) congruent to (a *;0 a) mod v.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Subgroup, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Matrix
Proof uses: Subgroup.copy, Subgroup.map, Subtype, Membership.mem, IsDedekindDomain.GL2.localIwahoriLevel, Subgroup.subtype, MonoidHom.ker, Units, IsLocalRing.ResidueField, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, IsDedekindDomain.GL2.localIwahoriLevel.char, Set.ofPred, And, LT.lt, WithZero, Multiplicative, Int, Valuation, Valued.v and 1 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
noncomputable def GL2.localTameLevel (v : HeightOneSpectrum (𝓞 F)) :
    Subgroup GL₂(v.adicCompletion F) :=
…
```
theorem IsDedekindDomain.GL2.localTameLevel.isOpen the clever way to prove this is a theorem of the form "if A is an open submonoid of R then Aˣ is an open subgroup of Rˣ" line 428 source
Source comment
the clever way to prove this is a theorem of the form "if A is an open submonoid of R then Aˣ is an open subgroup of Rˣ"

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, IsOpen, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Matrix, Subgroup, IsDedekindDomain.GL2.localTameLevel
Proof uses: IsOpen.inter, IsDedekindDomain.GL2.localIwahoriLevel, Set.ofPred, LT.lt, WithZero, Multiplicative, Int, Valuation, Valued.v, HSub.hSub, IsDedekindDomain.GL2.localIwahoriLevel.isOpen, Eq.mpr, MonoidWithZeroHom.ValueGroup₀, Subtype, Units, Membership.mem, MonoidWithZeroHom.valueGroup, Valuation.restrict, id, Eq and 14 more
106 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem GL2.localTameLevel.isOpen (v : HeightOneSpectrum (𝓞 F)) :
    IsOpen (X := GL₂(v.adicCompletion F)) (GL2.localTameLevel v) := by
…
```
Mentions: IsDedekindDomain.GL2.localTameLevel
lemma IsDedekindDomain.GL2.localIwahoriLevel.ker_char line 435 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Eq, Subgroup, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, Matrix, IsDedekindDomain.GL2.localIwahoriLevel, MonoidHom.ker, Units, IsLocalRing.ResidueField, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers and 3 more
Proof uses: Eq.mpr, Subgroup.copy, Subgroup.map, Subgroup.subtype, Set.ofPred, And, LT.lt, WithZero, Multiplicative, Int, Valuation, Valued.v, HSub.hSub, id, congrArg, IsDedekindDomain.GL2.localTameLevel.eq_1, Subgroup.copy_eq, Eq.symm, Subgroup.comap, Subgroup.comap_map_eq_self_of_injective and 1 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def IsDedekindDomain.GL2.localPTameLevel local U_1(v), defined as a subgroup of GL₂(Fᵥ) given by matrices in GL₂(𝒪ᵥ) congruent to (a *;0 b) mod v with p ∤ ord_{k(v)}(a/b) line 442 source
Source documentation
local U_1(v), defined as a subgroup of GL₂(Fᵥ) given by matrices in GL₂(𝒪ᵥ) congruent to (a *;0 b) mod v with p ∤ ord_{k(v)}(a/b).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Nat, Subgroup, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Matrix
Proof uses: Subgroup.map, Subtype, Membership.mem, IsDedekindDomain.GL2.localIwahoriLevel, Subgroup.subtype, MonoidHom.ker, MaximalPQuotient, Units, IsLocalRing.ResidueField, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, iInf, Subgroup.Normal, IsPGroup, HasQuotient.Quotient, MonoidHom.comp, MaximalPQuotient.mk, IsDedekindDomain.GL2.localIwahoriLevel.char
46 instances, coercions and auxiliary constants left out.
```
noncomputable def GL2.localPTameLevel (v : HeightOneSpectrum (𝓞 F)) (p : ℕ) :
    Subgroup (GL (Fin 2) (v.adicCompletion F)) :=
…
```
lemma IsDedekindDomain.GL2.localTameLevel_le_localPTameLevel line 446 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Nat, LE.le, Subgroup, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Matrix, IsDedekindDomain.GL2.localTameLevel, IsDedekindDomain.GL2.localPTameLevel
Proof uses: Eq.mpr, Subgroup.copy, Subgroup.map, Subtype, Membership.mem, IsDedekindDomain.GL2.localIwahoriLevel, Subgroup.subtype, MonoidHom.ker, Units, IsLocalRing.ResidueField, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, IsDedekindDomain.GL2.localIwahoriLevel.char, Set.ofPred, And, LT.lt, WithZero, Multiplicative, Int, Valuation and 16 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma IsDedekindDomain.GL2.localPTameLevel_le_localIwahoriLevel line 452 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Nat, LE.le, Subgroup, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Matrix, IsDedekindDomain.GL2.localPTameLevel, IsDedekindDomain.GL2.localIwahoriLevel
Proof uses: LE.le.trans, Subgroup.map, Subtype, Membership.mem, Subgroup.subtype, MonoidHom.ker, MaximalPQuotient, Units, IsLocalRing.ResidueField, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, iInf, Subgroup.Normal, IsPGroup, HasQuotient.Quotient, MonoidHom.comp, MaximalPQuotient.mk, IsDedekindDomain.GL2.localIwahoriLevel.char, MonoidHom.range, Subgroup.map_le_range and 6 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem IsDedekindDomain.GL2.localPTameLevel.isOpen line 457 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Nat, IsOpen, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Matrix, Subgroup, IsDedekindDomain.GL2.localPTameLevel
Proof uses: Subgroup.isOpen_mono, WithZero, Multiplicative, Int, IsDedekindDomain.GL2.localTameLevel, IsDedekindDomain.GL2.localTameLevel_le_localPTameLevel, IsDedekindDomain.GL2.localTameLevel.isOpen
66 instances, coercions and auxiliary constants left out.
theorem IsDedekindDomain.GL2.localPTameLevel.isCompact line 462 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Nat, IsCompact, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Matrix, Subgroup, IsDedekindDomain.GL2.localPTameLevel
Proof uses: IsCompact.of_isClosed_subset, IsDedekindDomain.GL2.localIwahoriLevel, IsDedekindDomain.GL2.localIwahoriLevel.isCompact, Subgroup.isClosed_of_isOpen, WithZero, Multiplicative, Int, IsDedekindDomain.GL2.localPTameLevel.isOpen, IsDedekindDomain.GL2.localPTameLevel_le_localIwahoriLevel
68 instances, coercions and auxiliary constants left out.
def IsDedekindDomain.GL2.localPTameLevelSubgroup line 471 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Nat, Subgroup, Units, IsDedekindDomain.HeightOneSpectrum.adicCompletion
Proof uses: Subgroup.map, Subtype, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Units.map, Algebra.algebraMap, MonoidHom.ker, MaximalPQuotient, IsLocalRing.ResidueField, iInf, Subgroup.Normal, IsPGroup, HasQuotient.Quotient, MonoidHom.comp, MaximalPQuotient.mk, IsLocalRing.residue
42 instances, coercions and auxiliary constants left out.
lemma IsDedekindDomain.GL2.localIwahoriLevel.ker_char_comp line 476 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Nat, Eq, Subgroup, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, Matrix, IsDedekindDomain.GL2.localIwahoriLevel, MonoidHom.ker, MaximalPQuotient, Units, IsLocalRing.ResidueField, ValuationSubring and 10 more
Proof uses: Eq.symm, Subgroup.comap, Subgroup.subtype, Subgroup.map, Subgroup.comap_map_eq_self_of_injective, Subtype.val_injective
68 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
instance IsDedekindDomain.(instance at line 480) line 480 source
lemma IsDedekindDomain.GL2.mem_localPTameLevel line 484 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Nat, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Iff, Membership.mem, Subgroup, Matrix, IsDedekindDomain.GL2.localPTameLevel, And, IsDedekindDomain.GL2.localIwahoriLevel, Exists, Ne, HDiv.hDiv, Units and 2 more
Proof uses: Iff.intro, And.intro, IsDedekindDomain.GL2.localPTameLevel_le_localIwahoriLevel, Eq, WithZero, Multiplicative, Int, Valuation, Valued.v, LE.le, LT.lt, Iff.mp, IsDedekindDomain.GL2.mem_localIwahoriLevel_iff_v, Exists.intro, Eq.mpr, Not, id, Eq.trans, Or, congrArg and 68 more
183 instances, coercions and auxiliary constants left out.

Tactic trace: 47 steps
Open to load the checked before-and-after goal states.
lemma IsDedekindDomain.GL2.localIwahoriLevel_le_normalizer_localPTameLevel line 521 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Nat, LE.le, Subgroup, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Matrix, IsDedekindDomain.GL2.localIwahoriLevel, Subgroup.normalizer, IsDedekindDomain.GL2.localPTameLevel
Proof uses: Eq.mpr, Subgroup.Normal, Subtype, Membership.mem, Subgroup.subgroupOf, id, Eq, congrArg, Eq.symm, propext, Subgroup.normal_subgroupOf_iff_le_normalizer, IsDedekindDomain.GL2.localPTameLevel_le_localIwahoriLevel, inferInstance
41 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def IsDedekindDomain.FiniteAdeleRing.toAdicCompletion line 534 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, AlgHom, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.HeightOneSpectrum.adicCompletion
Proof uses: RingHom, RestrictedProduct, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Filter.cofinite, RestrictedProduct.evalRingHom, AlgHom.mk
34 instances, coercions and auxiliary constants left out.
def IsDedekindDomain.FiniteAdeleRing.GL2.toAdicCompletion The canonical group homomorphism from GL_2(𝔸_F^∞) to the local component GL_2(F_v) for v a finite place line 545 source
Source documentation
The canonical group homomorphism from GL_2(𝔸_F^∞) to the local component GL_2(F_v) for v a finite place.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, MonoidHom, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Matrix
Proof uses: Units.map, RingHom.mapMatrix, AlgHom, IsDedekindDomain.FiniteAdeleRing.toAdicCompletion
41 instances, coercions and auxiliary constants left out.
```
noncomputable def GL2.toAdicCompletion
    (v : HeightOneSpectrum (𝓞 F)) :
    GL (Fin 2) (FiniteAdeleRing (𝓞 F) F) →* GL (Fin 2) (v.adicCompletion F) :=
…
```
lemma IsDedekindDomain.FiniteAdeleRing.GL2.continuous_toAdicCompletion line 550 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Continuous, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Matrix, MonoidHom, IsDedekindDomain.FiniteAdeleRing.GL2.toAdicCompletion
Proof uses: Units.continuous_map, RingHom.mapMatrix, AlgHom, IsDedekindDomain.FiniteAdeleRing.toAdicCompletion, Continuous.matrix_map, id, RingHom, continuous_id, RestrictedProduct.continuous_eval, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Filter.cofinite
56 instances, coercions and auxiliary constants left out.

def IsDedekindDomain.FiniteAdeleRing._root_.RestrictedProduct.mulSingleHom RestrictedProduct.mulSingle as a MonoidHom line 556 source

Source documentation

RestrictedProduct.mulSingle as a MonoidHom.

def _root_.RestrictedProduct.mulSingleHom {ι : Type*} {S : ι → Type*} {G : ι → Type*}
    [(i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i) [DecidableEq ι] [(i : ι) → Monoid (G i)]
    [∀ (i : ι), SubmonoidClass (S i) (G i)] (i : ι) :
    (G i) →* Πʳ i, [G i, A i] where
…

def IsDedekindDomain.FiniteAdeleRing.GL2.finiteAdeleIncl line 566 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, MonoidHom, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, IsDedekindDomain.FiniteAdeleRing, Matrix
Proof uses: MonoidHom.comp, RestrictedProduct, Units, Subgroup, Submonoid.units, Subsemiring.toSubmonoid, Subring.toSubsemiring, Subring.matrix, Valuation.integer, WithZero, Multiplicative, Int, Valued.v, Filter.cofinite, Subring, MulEquiv.toMonoidHom, ContinuousMulEquiv.toMulEquiv, ContinuousMulEquiv.symm, ContinuousMulEquiv.restrictedProductMatrixUnits, RestrictedProduct.mulSingleHom and 2 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma IsDedekindDomain.FiniteAdeleRing.GL2.toAdicCompletion_finiteAdeleIncl_of_ne line 573 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Ne, Eq, MonoidHom, IsDedekindDomain.FiniteAdeleRing, Matrix, IsDedekindDomain.FiniteAdeleRing.GL2.toAdicCompletion, IsDedekindDomain.FiniteAdeleRing.GL2.finiteAdeleIncl
Proof uses: DecidableEq, Classical.typeDecidableEq, Units.ext, Matrix.ext, id, of_eq_true, Pi.mulSingle, Eq.trans, True, congrFun', congrArg, Pi.mulSingle_eq_of_ne, Not, False, eq_false, not_false_eq_true, eq_self
45 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma IsDedekindDomain.FiniteAdeleRing.GL2.toAdicCompletion_finiteAdeleIncl_same line 583 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Eq, MonoidHom, IsDedekindDomain.FiniteAdeleRing, Matrix, IsDedekindDomain.FiniteAdeleRing.GL2.toAdicCompletion, IsDedekindDomain.FiniteAdeleRing.GL2.finiteAdeleIncl
Proof uses: DecidableEq, Classical.typeDecidableEq, Units.ext, Matrix.ext, id, of_eq_true, Pi.mulSingle, Eq.trans, True, congrFun', congrArg, Pi.mulSingle_eq_same, eq_self
40 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def IsDedekindDomain.FiniteAdeleRing.GL2.restrictedProduct GL_2(𝔸_F^∞) is isomorphic and homeomorphic to the restricted product of the local components GL_2(F_v) line 594 source
Source documentation
GL_2(𝔸_F^∞) is isomorphic and homeomorphic to the restricted product of the local components GL_2(F_v).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, ContinuousMulEquiv, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Matrix, RestrictedProduct, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Subgroup, Units, Submonoid.units, Subsemiring.toSubmonoid, Subring.toSubsemiring, IsDedekindDomain.M2.localFullLevel, Filter.cofinite
Proof uses: ContinuousMulEquiv.restrictedProductMatrixUnits, ValuationSubring.toSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, NumberField.isOpenAdicCompletionIntegers
48 instances, coercions and auxiliary constants left out.
```
noncomputable def GL2.restrictedProduct :
    GL₂(𝔸ᶠ[F]) ≃ₜ*
    Πʳ (v : HeightOneSpectrum (𝓞 F)),
      [GL₂(v.adicCompletion F), (M2.localFullLevel v).units] :=
…
```
Mentions: IsDedekindDomain.M2.localFullLevel
lemma IsDedekindDomain.FiniteAdeleRing.GL2.restrictedProduct_apply line 601 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, IsDedekindDomain.HeightOneSpectrum, Eq, IsDedekindDomain.HeightOneSpectrum.adicCompletion, RestrictedProduct, Subgroup, Units, Matrix, Submonoid.units, Subsemiring.toSubmonoid, Subring.toSubsemiring, IsDedekindDomain.M2.localFullLevel, Filter.cofinite and 4 more
Proof uses: rfl
82 instances, coercions and auxiliary constants left out.
lemma IsDedekindDomain.FiniteAdeleRing.GL2.ext line 604 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, IsDedekindDomain.HeightOneSpectrum, Eq, IsDedekindDomain.HeightOneSpectrum.adicCompletion, MonoidHom, Matrix, IsDedekindDomain.FiniteAdeleRing.GL2.toAdicCompletion
Proof uses: ContinuousMulEquiv.injective, RestrictedProduct, Subgroup, Units, Submonoid.units, Subsemiring.toSubmonoid, Subring.toSubsemiring, IsDedekindDomain.M2.localFullLevel, Filter.cofinite, IsDedekindDomain.FiniteAdeleRing.GL2.restrictedProduct, RestrictedProduct.ext, ContinuousMulEquiv, of_eq_true, Eq.trans, True, congrFun', congrArg, eq_self
61 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma IsDedekindDomain.FiniteAdeleRing.GL2.mul_comm_of_toAdicCompletion_eq_one line 610 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Eq, MonoidHom, Matrix, IsDedekindDomain.FiniteAdeleRing.GL2.toAdicCompletion, HMul.hMul, IsDedekindDomain.FiniteAdeleRing.GL2.finiteAdeleIncl
Proof uses: IsDedekindDomain.FiniteAdeleRing.GL2.ext, Ne, Or, eq_or_ne, of_eq_true, Eq.trans, True, congr, congrArg, map_mul, IsDedekindDomain.FiniteAdeleRing.GL2.toAdicCompletion_finiteAdeleIncl_same, one_mul, mul_one, eq_self, IsDedekindDomain.FiniteAdeleRing.GL2.toAdicCompletion_finiteAdeleIncl_of_ne, Not, False, eq_false, not_false_eq_true, congrFun'
50 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def IsDedekindDomain.FiniteAdeleRing.GL2.maximalCompact line 621 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Subgroup, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Matrix
Proof uses: iInf, IsDedekindDomain.HeightOneSpectrum, Subgroup.comap, IsDedekindDomain.HeightOneSpectrum.adicCompletion, IsDedekindDomain.FiniteAdeleRing.GL2.toAdicCompletion, IsDedekindDomain.GL2.localFullLevel
30 instances, coercions and auxiliary constants left out.
lemma IsDedekindDomain.FiniteAdeleRing.GL2.maximalCompact.isOpen line 624 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsOpen, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Matrix, Subgroup, IsDedekindDomain.FiniteAdeleRing.GL2.maximalCompact
Proof uses: Eq.mpr, RestrictedProduct, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Units, Submonoid.units, Subsemiring.toSubmonoid, Subring.toSubsemiring, IsDedekindDomain.M2.localFullLevel, Filter.cofinite, Set.preimage, Homeomorph, Homeomorph.symm, ContinuousMulEquiv.toHomeomorph, IsDedekindDomain.FiniteAdeleRing.GL2.restrictedProduct, id, Eq, congrArg, Eq.symm, propext and 33 more
75 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma IsDedekindDomain.FiniteAdeleRing.GL2.maximalCompact.isCompact line 631 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, IsCompact, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Matrix, Subgroup, IsDedekindDomain.FiniteAdeleRing.GL2.maximalCompact
Proof uses: Eq.mpr, RestrictedProduct, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Units, Submonoid.units, Subsemiring.toSubmonoid, Subring.toSubsemiring, IsDedekindDomain.M2.localFullLevel, Filter.cofinite, Set.preimage, Homeomorph, Homeomorph.symm, ContinuousMulEquiv.toHomeomorph, IsDedekindDomain.FiniteAdeleRing.GL2.restrictedProduct, id, Eq, congrArg, Eq.symm, propext and 44 more
87 instances, coercions and auxiliary constants left out.

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