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.
Co-authored-by: Jalex Stark <alexmaplegm@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
