No theorem Matrix.mulVec_sub

Stream: new members

[Adrian Wüthrich]

I found no theorem

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

there only is docs#Matrix.mulVec_add. Should I create a pull request for this?

[Kevin Buzzard]

At first glance it does indeed seem to be missing. Sure make a PR! Thanks!

[Adrian Wüthrich]

https://github.com/leanprover-community/mathlib4/pull/11392