Commit 2020-07-01 00:28 89f3bbc2

feat(data/matrix): std_basis_matrix (#3244) The definition of

def std_basis_matrix (i : m) (j : n) (a : α) : matrix m n α :=
(λ i' j', if i' = i ∧ j' = j then a else 0)

and associated lemmas, and some refactoring of src/ring_theory/matrix_algebra.lean to use it. This is work of @jalex-stark which I'm PR'ing as part of getting Cayley-Hamilton ready.