Defs

📁 Source: FLT/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean

Statistics

Metric	Count
Definitions unipotent, diagonal	2
Theorems unipotent_def, unipotent_inv, unipotent_mul	3
Total	5

Matrix.GeneralLinearGroup

Definitions

Name	Category	Theorems
diagonal 📖	CompOp	—

Matrix.GeneralLinearGroup.GL2

Definitions

Name	Category	Theorems
unipotent 📖	CompOp	5 math math: TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2.unipotent_mem_U1, TotallyDefiniteQuaternionAlgebra.WeightTwoAutomorphicForm.HeckeOperator.Local.GL2.unipotent_mul_diag_inv_mul_unipotent_mul_diag, unipotent_inv, unipotent_def, unipotent_mul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
unipotent_def 📖	mathematical	—	unipotent	—	—
unipotent_inv 📖	mathematical	—	unipotent	—	unipotent_def
unipotent_mul 📖	mathematical	—	unipotent	—	unipotent_def

---

← Back to Index