Local

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

Statistics

Metric	Count
Definitions diag, unipotent_mul_diag, U1, U1diagU1, unipotent_mul_diagU1	5
Theorems conjBy_diag, diag_def, unipotent_mem_U1, unipotent_mul_diag_inv_mul_unipotent_mul_diag, apply_mem_integer, apply_one_one_notMem_maximalIdeal, apply_one_zero_mem_maximalIdeal, apply_zero_zero_sub_apply_one_one_mem_maximalIdeal, conjBy_diag_mem_U1_iff_apply_zero_one_mem_ideal, isUnit_apply_one_one, bijOn_unipotent_mul_diagU1_U1diagU1, injOn_unipotent_mul_diagU1, mapsTo_unipotent_mul_diagU1_U1diagU1, surjOn_unipotent_mul_diagU1_U1diagU1	14
Total	19

TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local

Definitions

Name	Category	Theorems
U1 📖	CompOp	5 math math: GL2.unipotent_mem_U1, injOn_unipotent_mul_diagU1, mapsTo_unipotent_mul_diagU1_U1diagU1, bijOn_unipotent_mul_diagU1_U1diagU1, surjOn_unipotent_mul_diagU1_U1diagU1
U1diagU1 📖	CompOp	3 math math: mapsTo_unipotent_mul_diagU1_U1diagU1, bijOn_unipotent_mul_diagU1_U1diagU1, surjOn_unipotent_mul_diagU1_U1diagU1
unipotent_mul_diagU1 📖	CompOp	4 math math: injOn_unipotent_mul_diagU1, mapsTo_unipotent_mul_diagU1_U1diagU1, bijOn_unipotent_mul_diagU1_U1diagU1, surjOn_unipotent_mul_diagU1_U1diagU1

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bijOn_unipotent_mul_diagU1_U1diagU1 📖	mathematical	—	U1 unipotent_mul_diagU1 U1diagU1	—	mapsTo_unipotent_mul_diagU1_U1diagU1 injOn_unipotent_mul_diagU1 surjOn_unipotent_mul_diagU1_U1diagU1
injOn_unipotent_mul_diagU1 📖	mathematical	—	U1 unipotent_mul_diagU1	—	GL2.unipotent_mul_diag_inv_mul_unipotent_mul_diag U1.apply_mem_integer
mapsTo_unipotent_mul_diagU1_U1diagU1 📖	mathematical	—	U1 unipotent_mul_diagU1 U1diagU1	—	GL2.unipotent_mem_U1
surjOn_unipotent_mul_diagU1_U1diagU1 📖	mathematical	—	U1 unipotent_mul_diagU1 U1diagU1	—	U1.apply_mem_integer U1.isUnit_apply_one_one GL2.unipotent_mem_U1 U1.conjBy_diag_mem_U1_iff_apply_zero_one_mem_ideal Matrix.GeneralLinearGroup.GL2.unipotent_def

TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2

Definitions

Name	Category	Theorems
diag 📖	CompOp	3 math math: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.U1.conjBy_diag_mem_U1_iff_apply_zero_one_mem_ideal, diag_def, conjBy_diag
unipotent_mul_diag 📖	CompOp	1 math math: unipotent_mul_diag_inv_mul_unipotent_mul_diag

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conjBy_diag 📖	mathematical	—	diag	—	diag_def
diag_def 📖	mathematical	—	diag	—	diag.eq_1 Matrix.GeneralLinearGroup.diagonal.eq_1
unipotent_mem_U1 📖	mathematical	—	TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.U1 Matrix.GeneralLinearGroup.GL2.unipotent	—	IsDedekindDomain.GL2.mem_localFullLevel_iff_v_le_one_and_v_det_eq_one
unipotent_mul_diag_inv_mul_unipotent_mul_diag 📖	mathematical	—	unipotent_mul_diag Matrix.GeneralLinearGroup.GL2.unipotent	—	Matrix.GeneralLinearGroup.GL2.unipotent_inv Matrix.GeneralLinearGroup.GL2.unipotent_mul Matrix.GeneralLinearGroup.GL2.unipotent_def conjBy_diag

TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.U1

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_mem_integer 📖	—	TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.U1	—	—	IsDedekindDomain.GL2.v_le_one_of_mem_localFullLevel
apply_one_one_notMem_maximalIdeal 📖	mathematical	TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.U1	apply_mem_integer	—	apply_mem_integer apply_one_zero_mem_maximalIdeal IsDedekindDomain.HeightOneSpectrum.mem_completionIdeal_iff IsDedekindDomain.GL2.v_det_val_mem_localFullLevel_eq_one
apply_one_zero_mem_maximalIdeal 📖	mathematical	TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.U1	apply_mem_integer	—	apply_mem_integer IsDedekindDomain.HeightOneSpectrum.mem_completionIdeal_iff
apply_zero_zero_sub_apply_one_one_mem_maximalIdeal 📖	mathematical	TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.U1	apply_mem_integer	—	apply_mem_integer IsDedekindDomain.HeightOneSpectrum.mem_completionIdeal_iff
conjBy_diag_mem_U1_iff_apply_zero_one_mem_ideal 📖	mathematical	TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.U1	TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2.diag apply_mem_integer	—	apply_mem_integer TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2.conjBy_diag IsDedekindDomain.GL2.mem_localFullLevel_iff_v_le_one_and_v_det_eq_one IsDedekindDomain.HeightOneSpectrum.mem_completionIdeal_iff apply_one_zero_mem_maximalIdeal IsDedekindDomain.GL2.v_det_val_mem_localFullLevel_eq_one
isUnit_apply_one_one 📖	mathematical	TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.U1	apply_mem_integer	—	apply_mem_integer apply_one_one_notMem_maximalIdeal

---

← Back to Index