basic): make std_basis_matrix a linear map

Commit

4 years ago

chore(data/matrix/basic): make std_basis_matrix a linear map This bundles three lemmas into two

References

Author

eric-wieser

Parents