Transvection

📁 Source: FLT/Mathlib/LinearAlgebra/Matrix/Transvection.lean

Statistics

Metric	Count
Definitions ExistsListTransvecMulDiagonalMulListTransvec, map	2
Theorems baseChange_existsListTransvecEtc, exists_list_transvec_mul_diagonal_mul_list_transvec', mapMatrix_map_toMatrix_prod, mapMatrix_map_toMatrix_prod', map_toMatrix, toMatrix_map, diagonal_transvection_induction', diagonal_transvection_induction_of_det_unit	8
Total	10

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
diagonal_transvection_induction' 📖	—	Pivot.ExistsListTransvecMulDiagonalMulListTransvec	—	—	—
diagonal_transvection_induction_of_det_unit 📖	—	Pivot.ExistsListTransvecMulDiagonalMulListTransvec	—	—	diagonal_transvection_induction'

Matrix.Pivot

Definitions

Name	Category	Theorems
ExistsListTransvecMulDiagonalMulListTransvec 📖	MathDef	1 math math: exists_list_transvec_mul_diagonal_mul_list_transvec'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baseChange_existsListTransvecEtc 📖	—	ExistsListTransvecMulDiagonalMulListTransvec	—	—	Matrix.TransvectionStruct.mapMatrix_map_toMatrix_prod'
exists_list_transvec_mul_diagonal_mul_list_transvec' 📖	mathematical	—	ExistsListTransvecMulDiagonalMulListTransvec	—	—

Matrix.TransvectionStruct

Definitions

Name	Category	Theorems
map 📖	CompOp	4 math math: map_toMatrix, mapMatrix_map_toMatrix_prod', toMatrix_map, mapMatrix_map_toMatrix_prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapMatrix_map_toMatrix_prod 📖	mathematical	—	map	—	map_toMatrix
mapMatrix_map_toMatrix_prod' 📖	mathematical	—	map	—	mapMatrix_map_toMatrix_prod
map_toMatrix 📖	mathematical	—	map	—	toMatrix_map
toMatrix_map 📖	mathematical	—	map	—	—

---

← Back to Index