Commit 2024-03-19 17:09 5c4a670c

feat(Data/Matrix/Basic): add missing theorem mulVec_sub (#11392) Adds the following missing theorem

theorem mulVec_sub [Fintype n] (A : Matrix m n α) (x y : n → α) :
    A *ᵥ (x - y) = A *ᵥ x - A *ᵥ y

Currently there only is mulVec_sub. I asked about it here on zulip.