no goals
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : Semiring α
x : α
v : Fin n → α
w : o' → α
B : Fin n → o' → α
⊢ vecMul (vecCons x v) (↑of (vecCons w B)) = x • w + vecMul v (↑of B)
simp