Documentation Verification Report

Defs

📁 Source: FLT/AutomorphicForm/QuaternionAlgebra/Defs.lean

Statistics

Metric	Count
Definitions `Dfx`, `WeightTwoAutomorphicForm`, `add`, `addCommGroup`, `distribMulAction`, `group_smul`, `instAdd`, `instCoeFunForallDfx`, `instNeg`, `instSMul`, `instSMulDfx`, `instZero`, `module`, `mulAction`, `neg`, `ring_smul`, `toFun`, `zero`, `WeightTwoAutomorphicFormOfLevel`, `instAddCommGroup`, `instCoeFunForallDfx`, `instModule`, `toFun`, `incl₁`, `incl₂`, `instCommRingFiniteAdeleRingRingOfIntegers_fLT`, `instRingTensorProductFiniteAdeleRingRingOfIntegers_fLT`	27
Theorems `isOpen_smul`, `add_apply`, `ext`, `ext_iff`, `group_smul_apply`, `instContinuousConstSMulConjActOfContinuousMul`, `instSMulCommClassDfx`, `left_invt`, `neg_apply`, `right_invt`, `smul_apply`, `trivial_central_char`, `zero_apply`, `ext`, `ext_iff`, `left_invt`, `right_invt`, `range_incl₂_le_center`	18
Total	45

ConjAct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOpen_smul` 📖	—	—	—	—	`TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.instContinuousConstSMulConjActOfContinuousMul`

TotallyDefiniteQuaternionAlgebra

Definitions

Name	Category	Theorems
`Dfx` 📖	CompOp	8 math math: `WeightTwoAutomorphicForm.right_invt`, `WeightTwoAutomorphicForm.trivial_central_char`, `WeightTwoAutomorphicForm.instSMulCommClassDfx`, `WeightTwoAutomorphicForm.group_smul_apply`, `WeightTwoAutomorphicFormOfLevel.right_invt`, `range_incl₂_le_center`, `WeightTwoAutomorphicFormOfLevel.left_invt`, `WeightTwoAutomorphicForm.left_invt`
`WeightTwoAutomorphicForm` 📖	CompData	9 math math: `WeightTwoAutomorphicForm.smul_apply`, `WeightTwoAutomorphicForm.neg_apply`, `WeightTwoAutomorphicForm.zero_apply`, `WeightTwoAutomorphicForm.HeckeOperator.U_apply`, `WeightTwoAutomorphicForm.instSMulCommClassDfx`, `WeightTwoAutomorphicForm.group_smul_apply`, `WeightTwoAutomorphicForm.HeckeOperator.U_apply_eq_finsum_unipotent_mul_diag_image`, `WeightTwoAutomorphicForm.HeckeOperator.U_mul_aux`, `WeightTwoAutomorphicForm.add_apply`
`WeightTwoAutomorphicFormOfLevel` 📖	CompOp	5 math math: `WeightTwoAutomorphicForm.HeckeOperator.U_comm`, `WeightTwoAutomorphicForm.HeckeOperator.U_apply`, `WeightTwoAutomorphicForm.finiteDimensional`, `WeightTwoAutomorphicForm.HeckeOperator.U_apply_eq_finsum_unipotent_mul_diag_image`, `WeightTwoAutomorphicForm.HeckeOperator.U_mul`
`incl₁` 📖	CompOp	2 math math: `WeightTwoAutomorphicFormOfLevel.left_invt`, `WeightTwoAutomorphicForm.left_invt`
`incl₂` 📖	CompOp	2 math math: `WeightTwoAutomorphicForm.trivial_central_char`, `range_incl₂_le_center`
`instCommRingFiniteAdeleRingRingOfIntegers_fLT` 📖	CompOp	15 math math: `WeightTwoAutomorphicForm.HeckeOperator.unipotent_mul_diag_image_finite`, `WeightTwoAutomorphicForm.U1_compact`, `WeightTwoAutomorphicForm.right_invt`, `WeightTwoAutomorphicForm.HeckeOperator.bijOn_unipotent_mul_diagU1_U1diagU1`, `WeightTwoAutomorphicForm.trivial_central_char`, `WeightTwoAutomorphicForm.HeckeOperator.U_apply`, `WeightTwoAutomorphicForm.HeckeOperator.unipotent_mul_diag_inj`, `WeightTwoAutomorphicForm.group_smul_apply`, `WeightTwoAutomorphicForm.HeckeOperator.U_apply_eq_finsum_unipotent_mul_diag_image`, `WeightTwoAutomorphicFormOfLevel.right_invt`, `WeightTwoAutomorphicForm.HeckeOperator.U_mul_aux`, `range_incl₂_le_center`, `WeightTwoAutomorphicForm.U1_open`, `WeightTwoAutomorphicFormOfLevel.left_invt`, `WeightTwoAutomorphicForm.left_invt`
`instRingTensorProductFiniteAdeleRingRingOfIntegers_fLT` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`range_incl₂_le_center` 📖	mathematical	—	`Dfx` `instCommRingFiniteAdeleRingRingOfIntegers_fLT` `incl₂`	—	—

TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm

Definitions

Name	Category	Theorems
`add` 📖	CompOp	—
`addCommGroup` 📖	CompOp	3 math math: `HeckeOperator.U_apply`, `HeckeOperator.U_apply_eq_finsum_unipotent_mul_diag_image`, `HeckeOperator.U_mul_aux`
`distribMulAction` 📖	CompOp	—
`group_smul` 📖	CompOp	—
`instAdd` 📖	CompOp	1 math math: `add_apply`
`instCoeFunForallDfx` 📖	CompOp	—
`instNeg` 📖	CompOp	1 math math: `neg_apply`
`instSMul` 📖	CompOp	2 math math: `smul_apply`, `instSMulCommClassDfx`
`instSMulDfx` 📖	CompOp	5 math math: `HeckeOperator.U_apply`, `instSMulCommClassDfx`, `group_smul_apply`, `HeckeOperator.U_apply_eq_finsum_unipotent_mul_diag_image`, `HeckeOperator.U_mul_aux`
`instZero` 📖	CompOp	1 math math: `zero_apply`
`module` 📖	CompOp	—
`mulAction` 📖	CompOp	—
`neg` 📖	CompOp	—
`ring_smul` 📖	CompOp	—
`toFun` 📖	CompOp	9 math math: `smul_apply`, `right_invt`, `trivial_central_char`, `neg_apply`, `zero_apply`, `group_smul_apply`, `add_apply`, `ext_iff`, `left_invt`
`zero` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`toFun` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm` `instAdd`	—	—
`ext` 📖	—	`toFun`	—	—	—
`ext_iff` 📖	mathematical	—	`toFun`	—	`ext`
`group_smul_apply` 📖	mathematical	—	`toFun` `TotallyDefiniteQuaternionAlgebra.Dfx` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm` `instSMulDfx` `TotallyDefiniteQuaternionAlgebra.instCommRingFiniteAdeleRingRingOfIntegers_fLT`	—	—
`instContinuousConstSMulConjActOfContinuousMul` 📖	—	—	—	—	—
`instSMulCommClassDfx` 📖	mathematical	—	`TotallyDefiniteQuaternionAlgebra.Dfx` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm` `instSMulDfx` `instSMul`	—	`ext`
`left_invt` 📖	mathematical	—	`toFun` `TotallyDefiniteQuaternionAlgebra.Dfx` `TotallyDefiniteQuaternionAlgebra.instCommRingFiniteAdeleRingRingOfIntegers_fLT` `TotallyDefiniteQuaternionAlgebra.incl₁`	—	—
`neg_apply` 📖	mathematical	—	`toFun` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm` `instNeg`	—	—
`right_invt` 📖	mathematical	—	`TotallyDefiniteQuaternionAlgebra.Dfx` `TotallyDefiniteQuaternionAlgebra.instCommRingFiniteAdeleRingRingOfIntegers_fLT` `TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT` `toFun`	—	—
`smul_apply` 📖	mathematical	—	`toFun` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm` `instSMul`	—	—
`trivial_central_char` 📖	mathematical	—	`toFun` `TotallyDefiniteQuaternionAlgebra.Dfx` `TotallyDefiniteQuaternionAlgebra.instCommRingFiniteAdeleRingRingOfIntegers_fLT` `TotallyDefiniteQuaternionAlgebra.incl₂`	—	—
`zero_apply` 📖	mathematical	—	`toFun` `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm` `instZero`	—	—

TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicFormOfLevel

Definitions

Name	Category	Theorems
`instAddCommGroup` 📖	CompOp	5 math math: `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.U_comm`, `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.U_apply`, `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.finiteDimensional`, `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.U_apply_eq_finsum_unipotent_mul_diag_image`, `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.U_mul`
`instCoeFunForallDfx` 📖	CompOp	—
`instModule` 📖	CompOp	5 math math: `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.U_comm`, `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.U_apply`, `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.finiteDimensional`, `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.U_apply_eq_finsum_unipotent_mul_diag_image`, `TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.U_mul`
`toFun` 📖	CompOp	3 math math: `ext_iff`, `right_invt`, `left_invt`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`toFun`	—	—	`TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.ext`
`ext_iff` 📖	mathematical	—	`toFun`	—	`ext`
`left_invt` 📖	mathematical	—	`toFun` `TotallyDefiniteQuaternionAlgebra.Dfx` `TotallyDefiniteQuaternionAlgebra.instCommRingFiniteAdeleRingRingOfIntegers_fLT` `TotallyDefiniteQuaternionAlgebra.incl₁`	—	`TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.left_invt`
`right_invt` 📖	mathematical	—	`toFun` `TotallyDefiniteQuaternionAlgebra.Dfx` `TotallyDefiniteQuaternionAlgebra.instCommRingFiniteAdeleRingRingOfIntegers_fLT`	—	—

---

← Back to Index