Abstract

📁 Source: FLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Abstract.lean

Statistics

Metric	Count
Definitions HeckeOperator, HeckeOperator_addMonoidHom, HeckeOperator_toFun, instAddCommMonoidElemFixedPoints_fLT, instMulActionElemFixedPointsOfSMulCommClass_fLT, instSMulElemFixedPointsOfSMulCommClass_fLT, module	7
Theorems HeckeOperator_apply, comm, eq_finsum_quotient_out_of_bijOn', coe_add, coe_smul, coe_zero, bijOn_smul	7
Total	14

AbstractHeckeOperator

Definitions

Name	Category	Theorems
HeckeOperator 📖	CompOp	2 math math: comm, HeckeOperator_apply
HeckeOperator_addMonoidHom 📖	CompOp	—
HeckeOperator_toFun 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
HeckeOperator_apply 📖	mathematical	—	FixedPoints.instAddCommMonoidElemFixedPoints_fLT FixedPoints.module HeckeOperator	—	—
comm 📖	mathematical	—	FixedPoints.instAddCommMonoidElemFixedPoints_fLT FixedPoints.module HeckeOperator	—	HeckeOperator_apply eq_finsum_quotient_out_of_bijOn'
eq_finsum_quotient_out_of_bijOn' 📖	—	—	—	—	—

FixedPoints

Definitions

Name	Category	Theorems
instAddCommMonoidElemFixedPoints_fLT 📖	CompOp	4 math math: AbstractHeckeOperator.comm, AbstractHeckeOperator.HeckeOperator_apply, coe_zero, coe_add
instMulActionElemFixedPointsOfSMulCommClass_fLT 📖	CompOp	—
instSMulElemFixedPointsOfSMulCommClass_fLT 📖	CompOp	1 math math: coe_smul
module 📖	CompOp	2 math math: AbstractHeckeOperator.comm, AbstractHeckeOperator.HeckeOperator_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_add 📖	mathematical	—	instAddCommMonoidElemFixedPoints_fLT	—	—
coe_smul 📖	mathematical	—	instSMulElemFixedPointsOfSMulCommClass_fLT	—	—
coe_zero 📖	mathematical	—	instAddCommMonoidElemFixedPoints_fLT	—	—

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijOn_smul 📖	—	—	—	—	—

---

← Back to Index