mathlib

90475a9b - refactor(data/matrix): put std_basis_matrix in its own file (#9088)

refactor(data/matrix): put std_basis_matrix in its own file (#9088) The authors here are recovered from the git history. I've avoided the temptation to generalize typeclasses in this PR; the lemmas are copied to this file unmodified.