Theorem Matrix.matrix_eq_sum_stdBasisMatrix

Modification history

2024-10-25 13:43

Mathlib/Data/Matrix/Basis.lean

feat: Matrices over finite free modules are finite modules (#18098) …

Modified Matrix.matrix_eq_sum_stdBasisMatrix View on Github →

2024-08-11 23:33

Mathlib/Data/Matrix/Basis.lean

chore: clean up some naming around `Matrix.stdBasisMatrix` (#15693) …

Added Matrix.matrix_eq_sum_stdBasisMatrix View on Github →