Commit 2021-09-09 07:32 90475a9b

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.