Commit 2025-01-30 06:18 969f14dc

View on Github →

feat: ext lemmas for stdBasisMatrix (#21200) Additive and linear maps from matrices agree if they agree on stdBasisMatrix.

Estimated changes

Modified Mathlib/Data/Matrix/Basis.lean

added theorem Matrix.ext_addMonoidHom

added theorem Matrix.ext_linearMap

added def Matrix.stdBasisMatrixAddMonoidHom

added def Matrix.stdBasisMatrixLinearMap