Commit 2025-01-31 05:43 b4a286ec

View on Github →

feat: add lemmas about products of Matrix.stdBasisMatrix (#21204)

Estimated changes

Modified Mathlib/Data/Matrix/Hadamard.lean

added theorem Matrix.stdBasisMatrix_hadamard_stdBasisMatrix_eq

added theorem Matrix.stdBasisMatrix_hadamard_stdBasisMatrix_of_ne

Modified Mathlib/Data/Matrix/Kronecker.lean

added theorem Matrix.kroneckerMap_stdBasisMatrix_stdBasisMatrix

added theorem Matrix.kroneckerTMulBilinear_apply

added theorem Matrix.stdBasisMatrix_kroneckerTMul_stdBasisMatrix

added theorem Matrix.stdBasisMatrix_kronecker_stdBasisMatrix