Commit 2023-04-28 14:00 e14fff3b

View on Github →

feat: port LinearAlgebra.Matrix.Transvection (#3700)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/Transvection.lean

added theorem Matrix.Pivot.exists_isTwoBlockDiagonal_list_transvec_mul_mul_list_transvec

added theorem Matrix.Pivot.exists_isTwoBlockDiagonal_of_ne_zero

added theorem Matrix.Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec

added theorem Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal

added theorem Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal_aux

added theorem Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal_induction

added theorem Matrix.Pivot.isTwoBlockDiagonal_listTransvecCol_mul_mul_listTransvecRow

added def Matrix.Pivot.listTransvecCol

added theorem Matrix.Pivot.listTransvecCol_mul_last_col

added theorem Matrix.Pivot.listTransvecCol_mul_last_row

added theorem Matrix.Pivot.listTransvecCol_mul_last_row_drop

added theorem Matrix.Pivot.listTransvecCol_mul_mul_listTransvecRow_last_col

added theorem Matrix.Pivot.listTransvecCol_mul_mul_listTransvecRow_last_row

added def Matrix.Pivot.listTransvecRow

added theorem Matrix.Pivot.mul_listTransvecRow_last_col

added theorem Matrix.Pivot.mul_listTransvecRow_last_col_take

added theorem Matrix.Pivot.mul_listTransvecRow_last_row

added theorem Matrix.Pivot.reindex_exists_list_transvec_mul_mul_list_transvec_eq_diagonal

added theorem Matrix.TransvectionStruct.det_toMatrix_prod

added theorem Matrix.TransvectionStruct.inv_mul

added theorem Matrix.TransvectionStruct.mul_inv

added theorem Matrix.TransvectionStruct.mul_sumInl_toMatrix_prod

added theorem Matrix.TransvectionStruct.prod_mul_reverse_inv_prod

added def Matrix.TransvectionStruct.reindexEquiv

added theorem Matrix.TransvectionStruct.reverse_inv_prod_mul_prod

added def Matrix.TransvectionStruct.sumInl

added theorem Matrix.TransvectionStruct.sumInl_toMatrix_prod_mul

added def Matrix.TransvectionStruct.toMatrix

added theorem Matrix.TransvectionStruct.toMatrix_mk

added theorem Matrix.TransvectionStruct.toMatrix_reindexEquiv

added theorem Matrix.TransvectionStruct.toMatrix_reindexEquiv_prod

added theorem Matrix.TransvectionStruct.toMatrix_sumInl

added structure Matrix.TransvectionStruct

added theorem Matrix.det_transvection_of_ne

added theorem Matrix.diagonal_transvection_induction

added theorem Matrix.diagonal_transvection_induction_of_det_ne_zero

added theorem Matrix.mul_transvection_apply_of_ne

added theorem Matrix.mul_transvection_apply_same

added def Matrix.transvection

added theorem Matrix.transvection_mul_apply_of_ne

added theorem Matrix.transvection_mul_apply_same

added theorem Matrix.transvection_mul_transvection_same

added theorem Matrix.transvection_zero

added theorem Matrix.updateRow_eq_transvection