Commit 2024-08-11 23:33 d14d0e5b

View on Github →

chore: clean up some naming around Matrix.stdBasisMatrix (#15693) std_basis is a lean3-ism. In future we might want to rename this to Matrix.single.

Estimated changes

Modified Mathlib/Data/Matrix/Basis.lean

added theorem Matrix.matrix_eq_sum_stdBasisMatrix

deleted theorem Matrix.matrix_eq_sum_std_basis

added theorem Matrix.stdBasisMatrix_eq_single_vecMulVec_single

Modified Mathlib/RingTheory/MatrixAlgebra.lean

added theorem matrixEquivTensor_apply_stdBasisMatrix

deleted theorem matrixEquivTensor_apply_std_basis

Modified Mathlib/RingTheory/PolynomialAlgebra.lean