Commit 2023-04-04 13:03 e25fc659

View on Github →

feat: port Data.Matrix.Basis (#3243)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Matrix/Basis.lean

added theorem Matrix.StdBasisMatrix.apply_of_col_ne

added theorem Matrix.StdBasisMatrix.apply_of_ne

added theorem Matrix.StdBasisMatrix.apply_of_row_ne

added theorem Matrix.StdBasisMatrix.apply_same

added theorem Matrix.StdBasisMatrix.diag_same

added theorem Matrix.StdBasisMatrix.diag_zero

added theorem Matrix.StdBasisMatrix.mul_left_apply_of_ne

added theorem Matrix.StdBasisMatrix.mul_left_apply_same

added theorem Matrix.StdBasisMatrix.mul_of_ne

added theorem Matrix.StdBasisMatrix.mul_right_apply_of_ne

added theorem Matrix.StdBasisMatrix.mul_right_apply_same

added theorem Matrix.StdBasisMatrix.mul_same

added theorem Matrix.StdBasisMatrix.trace_eq

added theorem Matrix.StdBasisMatrix.trace_zero

added theorem Matrix.matrix_eq_sum_std_basis

added theorem Matrix.smul_stdBasisMatrix

added def Matrix.stdBasisMatrix

added theorem Matrix.stdBasisMatrix_add

added theorem Matrix.stdBasisMatrix_zero

added theorem Matrix.std_basis_eq_basis_mul_basis