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

87 declarations, 0 contain sorry, 0 declared as axioms

The Petersson inner product on quaternion modular forms.

Imports (4)

Imported by 1 file

FLT.lean

lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.star_χA line 46 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Membership.mem, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.UA, Eq, RingHom, starRingEnd and 4 more
Proof uses: Eq.symm, Complex.inv_eq_conj, And, LT.lt, HPow.hPow, Exists, Real, Norm.norm, Iff.mp, IsOfFinOrder, isOfFinOrder_iff_pow_eq_one, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.isOfFinOrder_χA_apply, Real.rpow_left_inj, of_eq_true, LE.le, Eq.mpr, Ne, Not, id, congrArg and 9 more
117 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.innerSummand The summand appearing in the Petersson inner product line 54 source
Source documentation
The summand appearing in the Petersson inner product.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, DoubleCoset.Quotient, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers and 6 more
Proof uses: HMul.hMul, Inv.inv, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.ΔIndex, Quotient.lift, DoubleCoset.setoid, RingHom, starRingEnd
69 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
def LevelStruct.innerSummand (ℒ : LevelStruct F R)
    (f g : ℒ.form D ℂ) (a : Dˣ＼GL₂(𝔸 F)／ℒ.UA) : ℂ :=
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.starRingEnd_innerSummand line 64 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, DoubleCoset.Quotient, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers and 10 more
Proof uses: Quotient, DoubleCoset.setoid, Quotient.mk, Exists, Quotient.mk_surjective, of_eq_true, Eq.trans, HMul.hMul, Inv.inv, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.ΔIndex, Set.range, MonoidHom, True, congr, congrArg, Quotient.lift, Quotient.lift.congr_simp, funext, mul_comm, id and 7 more
103 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.innerSummand_add_left line 72 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, Eq, DoubleCoset.Quotient, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing and 9 more
Proof uses: funext, Eq.mpr, id, congrArg, Pi.add_apply, Quotient, DoubleCoset.setoid, Quotient.mk, Exists, Quotient.mk_surjective, of_eq_true, HMul.hMul, Inv.inv, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.ΔIndex, Set.range, MonoidHom, RingHom, starRingEnd, Eq.trans, True and 10 more
100 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.innerSummand_smul_left line 82 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, Eq, DoubleCoset.Quotient, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing and 11 more
Proof uses: funext, Eq.mpr, id, congrArg, Pi.smul_apply, Quotient, DoubleCoset.setoid, Quotient.mk, Exists, Quotient.mk_surjective, HMul.hMul, Inv.inv, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.ΔIndex, Set.range, MonoidHom, congrFun', Quotient.lift, Quotient.lift.congr_simp, map_mul, Eq.refl and 26 more
150 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.(instance at line 91) line 91 source
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.(instance at line 92) line 92 source
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.(instance at line 96) line 96 source
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.(instance at line 99) line 99 source
def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.haarQuot The haar measure on GL₂(𝔸ᶠ[F]) that gives Π GL₂(𝒪ᵥ) measure one line 103 source
Source documentation
The haar measure on GL₂(𝔸ᶠ[F]) that gives Π GL₂(𝒪ᵥ) measure one.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, MeasureTheory.Measure, HasQuotient.Quotient, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Subgroup, Units, Matrix, MonoidHom.range, Units.map, Algebra.algebraMap
Proof uses: MeasureTheory.Measure.haarMeasure, QuotientGroup.leftRel, TopologicalSpace.PositiveCompacts.mk, TopologicalSpace.Compacts.mk, Subgroup.map, QuotientGroup.mk', IsDedekindDomain.FiniteAdeleRing.GL2.maximalCompact
57 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
def haarQuot : MeasureTheory.Measure (GL₂(𝔸ᶠ[F]) ⧸ 𝔸ˣ F) :=
…
```
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.(instance at line 110) line 110 source
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.(instance at line 111) line 111 source
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.(instance at line 113) line 113 source
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.haarQuot_mul_relIndex line 116 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, LE.le, Eq, ENNReal, HMul.hMul, MeasureTheory.Measure, HasQuotient.Quotient, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Subgroup, Units, Matrix, MonoidHom.range and 9 more
Proof uses: Eq.mpr, id, congrArg, mul_comm, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, outParam, HMul, NatCast, of_eq_true, Eq.trans, Max.max, True, MonoidHom.ker, Subgroup.relIndex_map_map, congr, QuotientGroup.ker_mk' and 16 more
131 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
def TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inner line 134 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form
Proof uses: HMul.hMul, ENNReal.toNNReal, MeasureTheory.Measure, HasQuotient.Quotient, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Subgroup, Units, Matrix, MonoidHom.range, Units.map, Algebra.algebraMap, Set, ENNReal, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.haarQuot, Subgroup.map and 8 more
62 instances, coercions and auxiliary constants left out.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.sum_filter_map_eq_ΔIndex_div_ΔIndex line 143 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, DivisionRing, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, LE.le, DoubleCoset.Quotient, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Matrix, Subgroup and 17 more
Proof uses: id, Eq.mpr, Quotient.lift, DoubleCoset.setoid, Min.min, HSMul.hSMul, ConjAct, Subgroup.pointwiseMulAction, MulEquiv, ConjAct.toConjAct, Inv.inv, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, Finset.sum_congr, Finset, Membership.mem, DoubleCoset.mk and 29 more
113 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inner_eq_of_map_le_map line 166 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, LE.le, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.map, Algebra.algebraMap, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, Eq and 2 more
Proof uses: Eq.symm, DoubleCoset.Quotient, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Matrix, Subgroup, MonoidHom.range, Units, IsQuaternionAlgebra.NumberField.WithRigidification.unitsIncl, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.UA, DoubleCoset.map, MonoidHom.id, le_rfl, sup_le_sup, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, Units.map and 103 more
201 instances, coercions and auxiliary constants left out.

Tactic trace: 52 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inner_eq_of_le line 218 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, LE.le, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, Eq, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inner, Subtype.mk and 2 more
Proof uses: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inner_eq_of_map_le_map, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.map_mono, Algebra.algebraMap
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inner_eq line 225 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, Eq, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inner, Subtype.mk
Proof uses: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.map, Algebra.algebraMap, Eq.ge, Submodule.restrictScalars, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form_map, Eq.mpr, Min.min, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form_anti, inf_le_left, Subtype.property, id, congrArg, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inner_eq_of_le, inf_le_right, Eq.refl, eq_of_heq, HEq, HEq.refl, Eq.symm, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inner_eq_of_map_le_map and 1 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 49 steps
Open to load the checked before-and-after goal states.
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.(instance at line 241) line 241 source
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.(instance at line 244) line 244 source
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.(instance at line 250) line 250 source
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.(instance at line 304) line 304 source
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.(instance at line 307) line 307 source
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.(instance at line 310) line 310 source
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.(instance at line 312) line 312 source
instance TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.(instance at line 315) line 315 source
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inner_def_of_mem line 320 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, Eq, Inner.inner, Complex.partialOrder, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inner, Subtype.mk
Proof uses: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inner_eq, Min.min, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.levelStruct
62 instances, coercions and auxiliary constants left out.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inner_coe line 324 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, Eq, Inner.inner, Complex.partialOrder
Proof uses: rfl
89 instances, coercions and auxiliary constants left out.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inner_def line 327 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, Eq, Inner.inner, Complex.partialOrder, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inner
Proof uses: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inner_eq, Min.min, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.levelStruct, LinearMap, RingHom.id, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formSubmodule, Submodule.subtype, Subtype.property
81 instances, coercions and auxiliary constants left out.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.Measure.conjAct_smul_of_isUnimodularGroup line 332 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Group, IsUnimodularGroup, MeasurableSpace, BorelSpace, MeasureTheory.Measure, MeasureTheory.Measure.IsHaarMeasure, MeasureTheory.Measure.Regular, ConjAct, Set, Eq, ENNReal, HSMul.hSMul, Set.smulSet
Proof uses: Eq.mpr, HMul.hMul, MonoidHom, NNReal, MeasureTheory.Measure.modularCharacter, MulEquiv, ConjAct.ofConjAct, id, congrArg, MeasureTheory.Measure.conjAct_smul, OfNat.ofNat, IsUnimodularGroup.modularCharacter_eq_one, of_eq_true, Eq.trans, True, congrFun', one_mul, eq_self
31 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.Subgroup.map_toConjAct_smul_mk' line 342 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Group, Subgroup, Subgroup.Normal, Eq, HasQuotient.Quotient, Subgroup.map, QuotientGroup.mk', HSMul.hSMul, ConjAct, Subgroup.pointwiseMulAction, MulEquiv, ConjAct.toConjAct
Proof uses: Eq.mpr, MonoidHom.comp, MonoidHom, Monoid.End, MulDistribMulAction.toMonoidEnd, id, congr, congrArg, Subgroup.map_map, Eq.refl
36 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm._root_.le_inv_smul_iff line 348 source
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm._root_.le_smul_sup line 353 source
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm._root_.smul_sup line 357 source
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.smul_UA line 365 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Eq, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.UA, HSMul.hSMul, ConjAct, Subgroup.pointwiseMulAction, MulEquiv, ConjAct.toConjAct
Proof uses: id, Eq.mpr, Max.max, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.U, MonoidHom.range, Units, Units.map, Algebra.algebraMap, congrArg, smul_sup, Max, Eq.rec, Eq.refl, Subgroup.conjAct_pointwise_smul_eq_self, Membership.mem, Subgroup.normalizer, Top.top, Iff.mpr, Subgroup.Normal, Subgroup.normalizer_eq_top_iff and 2 more
73 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.smul_Δ line 377 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, DivisionRing, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Eq, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.Δ, HSMul.hSMul, ConjAct, Subgroup.pointwiseMulAction and 3 more
Proof uses: Eq.mpr, Min.min, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.UA, Inv.inv, MonoidHom.range, Units, IsQuaternionAlgebra.NumberField.WithRigidification.unitsIncl, id, congr, congrArg, congrFun', TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.smul_UA, smul_inf, of_eq_true, Eq.trans, True, mul_inv_rev, SemigroupAction.mul_smul, smul_inv_smul, eq_self
82 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.Δ_mul line 385 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, CommRing, DivisionRing, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Eq, Subgroup, Matrix, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.Δ, HMul.hMul, HSMul.hSMul, ConjAct and 4 more
Proof uses: Eq.mpr, Min.min, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.UA, MonoidHom.range, Units, IsQuaternionAlgebra.NumberField.WithRigidification.unitsIncl, id, congrArg, Eq.trans, congrFun', TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.smul_UA, smul_inf, of_eq_true, True, congr, mul_inv_rev, SemigroupAction.mul_smul, inv_smul_smul, eq_self
83 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.inner_smul_eq_inner_inv_smul line 391 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Complex, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.FiniteAdeleRing, NumberField.RingOfIntegers, Eq, Inner.inner, Complex.partialOrder, HSMul.hSMul and 2 more
Proof uses: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct, Min.min, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.levelStruct, Eq.mpr, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inner, Subtype.mk, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, id, mem_of_le_of_mem, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form_anti, inf_le_left, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.mem_form, inf_le_right, congrArg, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inner_def_of_mem, Subtype.property, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.inner_eq_of_le, HMul.hMul and 77 more
210 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.inner_adicCompletion_smul line 424 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, DivisionRing, Algebra, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Complex, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Eq, Inner.inner, Complex.partialOrder and 3 more
Proof uses: Eq.trans, IsDedekindDomain.FiniteAdeleRing, MonoidHom, IsDedekindDomain.FiniteAdeleRing.GL2.finiteAdeleIncl, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.inner_smul_eq_inner_inv_smul, Eq.mpr, id, congrArg, Eq.symm, map_inv, Eq.refl
116 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.inner_heckeOperator line 429 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Eq, MonoidHom, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, Subgroup and 16 more
Proof uses: Finset, And, Set.BijOn, HasQuotient.Quotient, Set.image, HMul.hMul, Set, Set.mul, Singleton.singleton, Function.comp, Exists, exists_bijOn_mk_image_mul_singleton_and_mk_image_mul_singleton_inv, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.isOpen_US, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.isCompact_US, Iff.mp, Set.bijOn_comp_iff, Function.Injective.injOn, inv_injective, Eq.mpr, id and 27 more
218 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.adjoint_heckeOperatorL line 443 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Eq, MonoidHom, Subtype, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, Subgroup and 19 more
Proof uses: Eq.symm, Iff.mpr, Inner.inner, LinearMap.eq_adjoint_iff, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.inner_heckeOperator
162 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.isSymmetric_toModuleEnd_T line 465 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Not, Membership.mem, Finset, TotallyDefiniteQuaternionAlgebra.U₁Data.S, TotallyDefiniteQuaternionAlgebra.U₁Data.Q, LinearMap.IsSymmetric and 11 more
Proof uses: Eq.mpr, Eq, Inner.inner, LinearMap, RingHom.id, id, congrArg, LinearMap.IsSymmetric.eq_1, LinearEquiv, starRingEnd, LinearMap.adjoint, Eq.symm, propext, LinearMap.eq_adjoint_iff, eq_comm, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.heckeOperatorL, MonoidHom, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat and 50 more
157 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
def TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform Type parametrising eigen spaces of the anemic hecke algebra on S(U, ℂ) line 479 source
Source documentation
Type parametrising eigen spaces of the anemic hecke algebra on S(U, ℂ).

extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data
Proof uses: Subtype, AlgHom, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Membership.mem, Subalgebra, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic, Exists, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct, TotallyDefiniteQuaternionAlgebra.U₁, And, Ne, OfNat.ofNat, Eq, HSMul.hSMul
49 instances, coercions and auxiliary constants left out.
```
def Eigenform :=
…
```
def TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.eigenspace The eigenspace parametrised by an Eigenform line 485 source
Source documentation
The eigenspace parametrised by an Eigenform.

extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform, Submodule, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct, TotallyDefiniteQuaternionAlgebra.U₁
Proof uses: iInf, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Subalgebra, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic, Module.End.eigenspace, RingHom, Module.End, Module.toModuleEnd, AlgHom, Exists, And, Ne, OfNat.ofNat, Eq, HSMul.hSMul
71 instances, coercions and auxiliary constants left out.
```
def Eigenform.eigenspace (𝒻 : Eigenform D 𝒮) : Submodule ℂ S(U, ℂ) :=
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.U
instance TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.(instance at line 488) line 488 source
lemma TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.mem_eigenspace_iff line 490 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct, TotallyDefiniteQuaternionAlgebra.U₁ and 12 more
Proof uses: of_eq_true, Eq.trans, Subtype.mk, Not, True, congr, congrArg, Module.End.eigenspace, DistribSMul.toLinearMap, iInf, congrFun', RingHom, Module.End, Module.toModuleEnd, funext, Module.toModuleEnd_apply, OrderHom, ENat, Module.End.genEigenspace, forall_congr and 3 more
112 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
abbrev TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.eigenvalue The Tₚ-eigenvalue of an eigenform line 494 source
Source documentation
The Tₚ-eigenvalue of an eigenform.

extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Not, Membership.mem, Finset, TotallyDefiniteQuaternionAlgebra.U₁Data.S, TotallyDefiniteQuaternionAlgebra.U₁Data.Q
Proof uses: AlgHom, Subtype, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Subalgebra, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic, Exists, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct, TotallyDefiniteQuaternionAlgebra.U₁, And, Ne, OfNat.ofNat, Eq, HSMul.hSMul, Subtype.mk, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.T
56 instances, coercions and auxiliary constants left out.
```
abbrev Eigenform.eigenvalue (𝒻 : Eigenform D 𝒮) (v) (hvS : v ∉ 𝒮.S) (hvQ : v ∉ 𝒮.Q) : ℂ :=
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform
theorem TotallyDefiniteQuaternionAlgebra.HeckeAlgebra._root_.Algebra.coe_adjoin_induction line 499 source
lemma TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.mem_eigenspace_iff_T line 516 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct, TotallyDefiniteQuaternionAlgebra.U₁ and 13 more
Proof uses: Iff.trans, Subalgebra, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic, AlgHom, Exists, And, Ne, OfNat.ofNat, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.mem_eigenspace_iff, Iff.intro, Subtype.mk, Module.End, Algebra.adjoin, Union.union, Set, Set.ofPred, TotallyDefiniteQuaternionAlgebra.HeckeOperator.T, IsDedekindDomain.HeightOneSpectrum.adicCompletion, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers and 31 more
156 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.eigenvalue_injective line 528 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, Function.Injective, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Not, Membership.mem, Finset, TotallyDefiniteQuaternionAlgebra.U₁Data.S and 2 more
Proof uses: Eq, Subtype.ext, AlgHom, Subtype, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Subalgebra, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic, Exists, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct, TotallyDefiniteQuaternionAlgebra.U₁, And, Ne, OfNat.ofNat, HSMul.hSMul, AlgHom.adjoin_ext, Set.ofPred, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.T and 9 more
57 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.eigenSpace_ne_bot line 533 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform, Ne, Submodule, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct and 3 more
Proof uses: Eq.mpr, Exists, Not, Eq, OfNat.ofNat, id, Eq.trans, congrArg, funext, Exists.intro, Exists.choose, And, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Subalgebra, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic, HSMul.hSMul, AlgHom, Subtype.property, Iff.mpr, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.mem_eigenspace_iff and 3 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.exists line 539 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Not, Membership.mem, Finset, TotallyDefiniteQuaternionAlgebra.U₁Data.S, TotallyDefiniteQuaternionAlgebra.U₁Data.Q, Subtype and 16 more
Proof uses: Subalgebra, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic, Algebra.adjoin_induction, Set.ofPred, Set, Exists.intro, RingHom, Algebra.algebraMap, of_eq_true, Eq.trans, True, congr, congrArg, algebraMap_smul, eq_self, Algebra.adjoin, HAdd.hAdd, add_smul, HMul.hMul, Eq.mpr and 36 more
195 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
theorem TotallyDefiniteQuaternionAlgebra.HeckeAlgebra._root_.DirectSum.IsInternal.reindex line 573 source
theorem TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.isInternal line 619 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, DirectSum.IsInternal, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct and 2 more
Proof uses: DirectSum.IsInternal.reindex, IsDedekindDomain.HeightOneSpectrum, NumberField.RingOfIntegers, Set.ofPred, And, Not, Finset, TotallyDefiniteQuaternionAlgebra.U₁Data.S, TotallyDefiniteQuaternionAlgebra.U₁Data.Q, Classical.propDecidable, Eq, iInf, Module.End.eigenspace, RingHom, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Module.End, Module.toModuleEnd, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.T, Set, And.left and 45 more
127 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.cardinalMk_le line 640 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, LE.le, Cardinal, Cardinal.mk, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform, Module.finrank, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem and 4 more
Proof uses: Eq, Cardinal.lift, Module.rank, DirectSum, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.eigenspace, Eq.symm, LinearEquiv.lift_rank_eq, LinearEquiv.ofBijective, RingHom.id, DirectSum.coeLinearMap, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.isInternal, Eq.mpr, Cardinal.sum, id, congrArg, Eq.mp, congr, Cardinal.lift_natCast, Eq.trans, rank_directSum and 21 more
111 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
instance TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.(instance at line 651) line 651 source
abbrev TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.integers The subring of ℂ generated by the eigenvalues of an eigenform line 655 source
Source documentation
The subring of ℂ generated by the eigenvalues of an eigenform.

extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform, Subalgebra
Proof uses: AlgHom.range, Subtype, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Membership.mem, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic, AlgHom, Exists, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct, TotallyDefiniteQuaternionAlgebra.U₁, And, Ne, OfNat.ofNat, Eq, HSMul.hSMul
50 instances, coercions and auxiliary constants left out.
```
abbrev Eigenform.integers (𝒻 : Eigenform D 𝒮) : Subalgebra R ℂ := 𝒻.1.range
```
Mentions: TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform
abbrev TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.toIntegers The induced map of an Eigenform from an hecke algebra to its integers line 658 source
Source documentation
The induced map of an Eigenform from an hecke algebra to its integers.

extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform, AlgHom, Subtype, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Membership.mem, Subalgebra, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.integers
Proof uses: AlgHom.rangeRestrict, Exists, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct, TotallyDefiniteQuaternionAlgebra.U₁, And, Ne, OfNat.ofNat, Eq, HSMul.hSMul
57 instances, coercions and auxiliary constants left out.
```
abbrev Eigenform.toIntegers (𝒻 : Eigenform D 𝒮) : anemic D 𝒮 →ₐ[R] 𝒻.integers := 𝒻.1.rangeRestrict
```
Mentions: TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic
def TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.prime The (minimal) prime corresponding to an eigenform line 661 source
Source documentation
The (minimal) prime corresponding to an eigenform.

extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform, PrimeSpectrum, Subtype, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Membership.mem, Subalgebra, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic
Proof uses: PrimeSpectrum.mk, RingHom.ker, RingHom, AlgHom.toRingHom, AlgHom, Exists, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct, TotallyDefiniteQuaternionAlgebra.U₁, And, Ne, OfNat.ofNat, Eq, HSMul.hSMul
61 instances, coercions and auxiliary constants left out.
```
def Eigenform.prime (𝒻 : Eigenform D 𝒮) : PrimeSpectrum (anemic D 𝒮) :=
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic
def TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.primeQuotient 𝕋/𝔭(f) = 𝒪(f) line 665 source
Source documentation
𝕋/𝔭(f) = 𝒪(f)

extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform, AlgEquiv, HasQuotient.Quotient, Subtype, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Membership.mem, Subalgebra, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic and 4 more
Proof uses: Ideal.quotientKerEquivRange, AlgHom, Exists, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct, TotallyDefiniteQuaternionAlgebra.U₁, And, Ne, OfNat.ofNat, Eq, HSMul.hSMul
64 instances, coercions and auxiliary constants left out.
```
def Eigenform.primeQuotient (𝒻 : Eigenform D 𝒮) :
    (anemic D 𝒮 ⧸ 𝒻.prime.asIdeal) ≃ₐ[R] 𝒻.integers := Ideal.quotientKerEquivRange _
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic
lemma TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.primeQuotient_mk line 669 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform, Subtype, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Membership.mem, Subalgebra, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic, Eq, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.integers and 10 more
Proof uses: rfl
55 instances, coercions and auxiliary constants left out.
lemma TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.toIntegers_surjective line 672 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform, Function.Surjective, Subtype, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Membership.mem, Subalgebra, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.integers and 2 more
Proof uses: AlgHom.rangeRestrict_surjective, Exists, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct, TotallyDefiniteQuaternionAlgebra.U₁, And, Ne, OfNat.ofNat, Eq, HSMul.hSMul
59 instances, coercions and auxiliary constants left out.
instance TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.(instance at line 675) line 675 source
instance TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.(instance at line 678) line 678 source
instance TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.(instance at line 681) line 681 source
instance TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.(instance at line 684) line 684 source
instance TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.(instance at line 687) line 687 source
def TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.toProdEigenform The embedding of the anemic Hecke algebra into a product of domains, indexed by eigenforms line 692 source
Source documentation
The embedding of the anemic Hecke algebra into a product of domains, indexed by eigenforms.

extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, AlgHom, Subtype, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Membership.mem, Subalgebra, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.integers
Proof uses: AlgHom.pi, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.toIntegers
28 instances, coercions and auxiliary constants left out.
```
def toProdEigenform : anemic D 𝒮 →ₐ[R] Π (𝒻 : Eigenform D 𝒮), 𝒻.integers :=
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform
lemma TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.toProdEigenform_apply line 696 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, Subtype, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Membership.mem, Subalgebra, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform, Eq, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.integers and 3 more
Proof uses: rfl
34 instances, coercions and auxiliary constants left out.
lemma TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.smul_formTensorScalar_tmul line 699 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Subtype, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Membership.mem, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct, TotallyDefiniteQuaternionAlgebra.U₁ and 7 more
Proof uses: of_eq_true, LinearMap, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formMap, LinearMap.toSpanSingleton, Eq.trans, True, congrFun', congrArg, eq_self
107 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.toProdEigenform_injective line 707 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, FaithfulSMul, Function.Injective, Subtype, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Membership.mem, Subalgebra, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform and 3 more
Proof uses: Iff.mpr, Eq, OfNat.ofNat, injective_iff_map_eq_zero, outParam, MonoidHom, MonoidHom.id, Subtype.ext, FaithfulSMul.eq_of_smul_eq_smul, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct, TotallyDefiniteQuaternionAlgebra.U₁, iSup, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.eigenspace, Eq.ge, Top.top, DirectSum.IsInternal.submodule_iSup_eq_top, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.isInternal and 20 more
113 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
instance TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.(instance at line 719) line 719 source
instance TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.(instance at line 724) line 724 source
theorem TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Algebra.lsmul_injective_of_faithfulSMul line 730 source
standard axioms: Quot.sound, propext what this means
Statement uses: CommSemiring, Semiring, Algebra, AddCommMonoid, Module, IsScalarTower, SMulCommClass, FaithfulSMul, Function.Injective, Module.End, AlgHom, Algebra.lsmul
Proof uses: Eq, FaithfulSMul.eq_of_smul_eq_smul, id, HSMul.hSMul, congrArg, RingHom.id
35 instances, coercions and auxiliary constants left out.
theorem TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Algebra.TensorProduct.lTensor_injective line 738 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommSemiring, Algebra, Semiring, IsScalarTower, Module.Flat, AlgHom, Function.Injective, TensorProduct, Algebra.TensorProduct.lTensor
Proof uses: Module.Flat.lTensor_preserves_injective_linearMap, AlgHom.toLinearMap
15 instances, coercions and auxiliary constants left out.
lemma TotallyDefiniteQuaternionAlgebra.HeckeAlgebra._root_.AlgHom.map_zero line 746 source
lemma TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.pi_lift_injective line 749 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, FaithfulSMul, Function.Injective, TensorProduct, Subtype, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Membership.mem, Subalgebra, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic and 17 more
Proof uses: Iff.mpr, injective_iff_map_eq_zero, outParam, MonoidHom, MonoidHom.id, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Algebra.TensorProduct.lTensor_injective, Module.End, Algebra.lsmul, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Algebra.lsmul_injective_of_faithfulSMul, LinearEquiv.injective, LinearMap, RingHom.id, lTensorHomEquivHomLTensor, Algebra.TensorProduct.lTensor, LinearMap.liftBaseChangeEquiv, LinearEquiv, LinearMap.ext, LinearEquiv.symm, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.formTensorScalar, LinearEquiv.surjective and 45 more
276 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
def TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Pi.subalgebraEquiv There is a correspondence between K-subalgebras of Kⁿ and partitions of n, where for each set in the partition we take the diagonal subalgebra line 788 source
Source documentation
There is a correspondence between K-subalgebras of Kⁿ and partitions of n, where for each set in the partition we take the diagonal subalgebra.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finite, Field, Equiv, Subalgebra, Setoid
Proof uses: Equiv.mk, Setoid.mk, Membership.mem, Eq, Subalgebra.mk, Subsemiring.mk, Submonoid.mk, Subsemigroup.mk, Set.ofPred, HasEquiv.Equiv, Set
29 instances, coercions and auxiliary constants left out.

Tactic trace: 57 steps
Open to load the checked before-and-after goal states.
```
def Pi.subalgebraEquiv (n K : Type*) [Finite n] [Field K] : Subalgebra K (n → K) ≃ Setoid n where
…
```
lemma TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Pi.subalgebraEquiv_top line 834 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finite, Field, Eq, Setoid, Equiv, Subalgebra, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Pi.subalgebraEquiv, Top.top, Bot.bot
Proof uses: Setoid.ext, Iff.intro, Eq.mpr, id, Eq.mp, Pi.single, Classical.propDecidable, OfNat.ofNat, Eq.trans, Not, ite, congr, congrArg, Pi.single_apply, Pi.single_eq_same, False, implies_congr, Eq.refl, of_eq_true, Membership.mem and 2 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.tensorEquivPi The complex anemic Hecke algebra is isomorphic to a product of copies of ℂ's, one for each eigenform line 843 source
Source documentation
The complex anemic Hecke algebra is isomorphic to a product of copies of ℂ's, one for each eigenform.

extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, FaithfulSMul, AlgEquiv, TensorProduct, Subtype, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Membership.mem, Subalgebra, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic and 1 more
Proof uses: AlgEquiv.ofBijective, AlgHom.pi, Algebra.TensorProduct.lift, AlgHom.id, AlgHom, Exists, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct, TotallyDefiniteQuaternionAlgebra.U₁, And, Ne, OfNat.ofNat, Eq, HSMul.hSMul
86 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def tensorEquivPi : ℂ ⊗[R] anemic D 𝒮 ≃ₐ[ℂ] (Eigenform D 𝒮 → ℂ) := by
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform
lemma TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.tensorEquivPi_tmul_apply line 851 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, FaithfulSMul, Subtype, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Membership.mem, Subalgebra, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform, Eq and 15 more
Proof uses: rfl
91 instances, coercions and auxiliary constants left out.
def TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.equivAlgHom The eigenforms corresponds exactly to maps from 𝕋 to ℂ line 855 source
Source documentation
The eigenforms corresponds exactly to maps from 𝕋 to ℂ.

extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, FaithfulSMul, Equiv, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform, AlgHom, Subtype, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Membership.mem, Subalgebra and 1 more
Proof uses: Equiv.ofBijective, Exists, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, Submodule, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct, TotallyDefiniteQuaternionAlgebra.U₁, And, Ne, OfNat.ofNat, Eq, HSMul.hSMul
60 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
def Eigenform.equivAlgHom : Eigenform D 𝒮 ≃ (anemic D 𝒮 →ₐ[R] ℂ) :=
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic
lemma TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.under_prime line 875 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, FaithfulSMul, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform, Eq, Ideal, Ideal.under, Subtype, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Membership.mem and 5 more
Proof uses: Iff.mp, LE.le, le_bot_iff, Submodule, Eq.mpr, OfNat.ofNat, id, Eq.mp, Eq.trans, Ideal.comap, RingHom, Algebra.algebraMap, RingHom.ker, AlgHom, Exists, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LevelStruct.form, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.LocalLevelStruct.toStruct, TotallyDefiniteQuaternionAlgebra.U₁, And and 5 more
83 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.prime_mem_minimalPrimes line 879 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, FaithfulSMul, IsNoetherianRing, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform, Membership.mem, Ideal, Subtype, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Subalgebra and 5 more
Proof uses: And.intro, And, Ideal.IsPrime, LE.le, Bot.bot, inferInstance, bot_le, Eq.ge, Algebra.QuasiFiniteAt.eq_of_le_of_under_eq, le_antisymm, Ideal.under, Ideal.comap_mono, RingHom, Algebra.algebraMap, Eq.mpr, id, Eq, congrArg, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.under_prime, Ideal.primeCompl
46 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.exists_le_of_isPrime linter complained that [P.IsPrime] wasn't needed, so this lemma is now poorly-named line 887 source
Source comment
linter complained that [P.IsPrime] wasn't needed, so this lemma is now poorly-named

extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, FaithfulSMul, Ideal, Subtype, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Membership.mem, Subalgebra, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic, Eq and 7 more
Proof uses: Nontrivial, TensorProduct, HasQuotient.Quotient, Algebra.TensorProduct.nontrivial_of_algebraMap_injective_of_flat_left, Eq.mpr, Function.Injective, RingHom, Algebra.algebraMap, RingHom.ker, id, congrArg, propext, RingHom.injective_iff_ker_eq_bot, RingHom.comp, Ideal.Quotient.alg_map_eq, Ideal.comap, Eq.symm, RingHom.comap_ker, Ideal.Quotient.mk, Ideal.Quotient.algebraMap_eq and 68 more
161 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma Eigenform.exists_le_of_isPrime (P : Ideal (anemic D 𝒮)) (hP : P.under R = ⊥) :
    ∃ 𝒻 : Eigenform D 𝒮, P ≤ 𝒻.prime.asIdeal := by
…
```
Mentions: TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform
lemma TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.exists_of_isPrime line 912 source
extra axioms: knownin1980s what this means
Statement uses: Field, NumberField, CommRing, Algebra, Complex, DivisionRing, IsQuaternionAlgebra.NumberField.WithRigidification, IsQuaternionAlgebra, NumberField.IsTotallyReal, IsQuaternionAlgebra.IsTotallyDefinite, Nat, TotallyDefiniteQuaternionAlgebra.U₁Data, FaithfulSMul, IsNoetherianRing, Ideal, Subtype, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra, Membership.mem, Subalgebra, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.anemic and 8 more
Proof uses: LE.le, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.exists_le_of_isPrime, Exists.intro, LE.le.antisymm, And.right, And, TotallyDefiniteQuaternionAlgebra.HeckeAlgebra.Eigenform.prime_mem_minimalPrimes, And.intro, bot_le
41 instances, coercions and auxiliary constants left out.

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