mathlib

f95f216f - feat(linear_algebra/std_basis): add matrix.std_basis_eq_std_basis_matrix (#9216)

feat(linear_algebra/std_basis): add matrix.std_basis_eq_std_basis_matrix (#9216) As suggested in #9072 by @eric-wieser, we modify `matrix.std_basis` to use the more familiar `n × m` as the index of the basis and we prove that the `(i,j)`-th element of this basis is `matrix.std_basis_matrix i j 1`.