Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.elementary_eq_basis_mul_basis

Modification history

2020-07-10 05:40
src/data/matrix/basic.lean
feat(data/matrix): add matrix.map and supporting lemmas (#3352) …
Deleted matrix.elementary_eq_basis_mul_basisView on Github →
2020-07-01 00:28
src/data/matrix/basic.lean
feat(data/matrix): std_basis_matrix (#3244) …
Added matrix.elementary_eq_basis_mul_basisView on Github →