Commit 2024-05-02 00:23 d9f14974

View on Github →

feat(Data/Matrix): Equalities relating mulVec and smul (#12538) These lemmas should make working with vectors easier in some cases. Check this related Zulip topic.

Estimated changes

Modified Mathlib/Data/Matrix/Basic.lean

added theorem Matrix.diagonal_const_mulVec

added theorem Matrix.intCast_mulVec

added theorem Matrix.natCast_mulVec

added theorem Matrix.ofNat_mulVec

added theorem Matrix.vecMul_diagonal_const

added theorem Matrix.vecMul_intCast

added theorem Matrix.vecMul_natCast

added theorem Matrix.vecMul_ofNat