Documentation Verification Report

Concrete

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

Statistics

Metric	Count
Definitions `HeckeAlgebra`, `T`, `U`, `instAlgebra`, `instCommRing`, `instRing`, `T`, `U`, `U1diagU1`, `diag`, `instDecidableEqHeightOneSpectrumRingOfIntegers`, `instDistribSMulUnitsTensorProductFiniteAdeleRingRingOfIntegers`, `unipotent_mul_diag`, `unipotent_mul_diag_image`, `U1`	15
Theorems `mul`, `mk_image_finite_of_compact_of_open`, `U_apply`, `U_apply_eq_finsum_unipotent_mul_diag_image`, `U_comm`, `U_mul`, `U_mul_aux`, `bijOn_unipotent_mul_diagU1_U1diagU1`, `quot_top_finite`, `unipotent_mul_diag_image_finite`, `unipotent_mul_diag_inj`, `U1_compact`, `U1_open`	13
Total	28
⚠️ With sorry `U_mul_aux`, `bijOn_unipotent_mul_diagU1_U1diagU1`, `U1_compact`, `U1_open`	4

Ne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul` 📖	—	—	—	—	—

QuotientGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk_image_finite_of_compact_of_open` 📖	—	—	—	—	—

TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm

Definitions

Name	Category	Theorems
`HeckeAlgebra` 📖	CompOp	—
`U1` 📖	CompOp	7 math math: `HeckeOperator.U_comm`, `U1_compact`, `HeckeOperator.bijOn_unipotent_mul_diagU1_U1diagU1`, `HeckeOperator.U_apply`, `HeckeOperator.U_apply_eq_finsum_unipotent_mul_diag_image`, `HeckeOperator.U_mul`, `U1_open`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`U1_compact` 📖 ⚠️	mathematical	—	`TotallyDefiniteQuaternionAlgebra.instCommRingFiniteAdeleRingRingOfIntegers_fLT` `TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT` `IsQuaternionAlgebra.instFinite` `U1`	—	`IsQuaternionAlgebra.instFinite`
`U1_open` 📖 ⚠️	mathematical	—	`TotallyDefiniteQuaternionAlgebra.instCommRingFiniteAdeleRingRingOfIntegers_fLT` `TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT` `IsQuaternionAlgebra.instFinite` `U1`	—	`IsQuaternionAlgebra.instFinite`

TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeAlgebra

Definitions

Name	Category	Theorems
`T` 📖	CompOp	—
`U` 📖	CompOp	—
`instAlgebra` 📖	CompOp	—
`instCommRing` 📖	CompOp	—
`instRing` 📖	CompOp	—

TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator

Definitions

Name	Category	Theorems
`T` 📖	CompOp	—
`U` 📖	CompOp	4 math math: `U_comm`, `U_apply`, `U_apply_eq_finsum_unipotent_mul_diag_image`, `U_mul`
`U1diagU1` 📖	CompOp	2 math math: `bijOn_unipotent_mul_diagU1_U1diagU1`, `U_apply`
`diag` 📖	CompOp	—
`instDecidableEqHeightOneSpectrumRingOfIntegers` 📖	CompOp	—
`instDistribSMulUnitsTensorProductFiniteAdeleRingRingOfIntegers` 📖	CompOp	—
`unipotent_mul_diag` 📖	CompOp	2 math math: `unipotent_mul_diag_inj`, `U_mul_aux`
`unipotent_mul_diag_image` 📖	CompOp	3 math math: `unipotent_mul_diag_image_finite`, `bijOn_unipotent_mul_diagU1_U1diagU1`, `U_apply_eq_finsum_unipotent_mul_diag_image`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`U_apply` 📖	mathematical	—	`TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm` `IsQuaternionAlgebra.instFinite` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicFormOfLevel` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.U1` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicFormOfLevel.instAddCommGroup` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicFormOfLevel.instModule` `U` `TotallyDefiniteQuaternionAlgebra.instCommRingFiniteAdeleRingRingOfIntegers_fLT` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.addCommGroup` `U1diagU1` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.instSMulDfx`	—	`IsQuaternionAlgebra.instFinite`
`U_apply_eq_finsum_unipotent_mul_diag_image` 📖	mathematical	—	`TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm` `IsQuaternionAlgebra.instFinite` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicFormOfLevel` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.U1` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicFormOfLevel.instAddCommGroup` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicFormOfLevel.instModule` `U` `TotallyDefiniteQuaternionAlgebra.instCommRingFiniteAdeleRingRingOfIntegers_fLT` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.addCommGroup` `unipotent_mul_diag_image` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.instSMulDfx`	—	`IsQuaternionAlgebra.instFinite` `U_apply` `AbstractHeckeOperator.eq_finsum_quotient_out_of_bijOn'` `bijOn_unipotent_mul_diagU1_U1diagU1`
`U_comm` 📖	mathematical	—	`TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicFormOfLevel` `IsQuaternionAlgebra.instFinite` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.U1` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicFormOfLevel.instAddCommGroup` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicFormOfLevel.instModule` `U`	—	`IsQuaternionAlgebra.instFinite` `Ne.mul` `U_mul`
`U_mul` 📖	mathematical	—	`TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicFormOfLevel` `IsQuaternionAlgebra.instFinite` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.U1` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicFormOfLevel.instAddCommGroup` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicFormOfLevel.instModule` `U` `Ne.mul`	—	`IsQuaternionAlgebra.instFinite` `Ne.mul` `U_apply_eq_finsum_unipotent_mul_diag_image` `unipotent_mul_diag_image_finite` `U_mul_aux`
`U_mul_aux` 📖 ⚠️	mathematical	—	`TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm` `IsQuaternionAlgebra.instFinite` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.addCommGroup` `TotallyDefiniteQuaternionAlgebra.instCommRingFiniteAdeleRingRingOfIntegers_fLT` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.instSMulDfx` `unipotent_mul_diag` `Ne.mul`	—	`IsQuaternionAlgebra.instFinite` `Ne.mul`
`bijOn_unipotent_mul_diagU1_U1diagU1` 📖 ⚠️	mathematical	—	`TotallyDefiniteQuaternionAlgebra.instCommRingFiniteAdeleRingRingOfIntegers_fLT` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.U1` `unipotent_mul_diag_image` `U1diagU1`	—	—
`quot_top_finite` 📖	—	—	—	—	`unipotent_mul_diag_image_finite`
`unipotent_mul_diag_image_finite` 📖	mathematical	—	`TotallyDefiniteQuaternionAlgebra.instCommRingFiniteAdeleRingRingOfIntegers_fLT` `unipotent_mul_diag_image`	—	`bijOn_unipotent_mul_diagU1_U1diagU1` `QuotientGroup.mk_image_finite_of_compact_of_open` `IsQuaternionAlgebra.instFinite` `TensorProduct.RightActions.instIsTopologicalRing_fLT_1` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.U1_compact` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.U1_open`
`unipotent_mul_diag_inj` 📖	mathematical	—	`TotallyDefiniteQuaternionAlgebra.instCommRingFiniteAdeleRingRingOfIntegers_fLT` `unipotent_mul_diag`	—	`RestrictedProduct.mulSingle_eq_same`

---

← Back to Index