no goals
l : Type ?u.913128
m : Type u_1
n : Type u_2
o : Type ?u.913137
m' : o → Type ?u.913142
n' : o → Type ?u.913147
R : Type ?u.913150
S : Type ?u.913153
α : Type v
β : Type w
γ : Type ?u.913160
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype m
A B : Matrix m n α
x : m → α
⊢ vecMul x (A - B) = vecMul x A - vecMul x B
simp [sub_eq_add_neg, vecMul_add, vecMul_neg]