case h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : Semiring α
v : Fin (Nat.succ n) → α
w : o' → α
B : Fin n → o' → α
i : o'
⊢ vecMul v (↑of (vecCons w B)) i = (vecHead v • w + vecMul (vecTail v) (↑of B)) i
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : Semiring α
v : Fin (Nat.succ n) → α
w : o' → α
B : Fin n → o' → α
⊢ vecMul v (↑of (vecCons w B)) = vecHead v • w + vecMul (vecTail v) (↑of B)
ext i
no goals
case h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : Semiring α
v : Fin (Nat.succ n) → α
w : o' → α
B : Fin n → o' → α
i : o'
⊢ vecMul v (↑of (vecCons w B)) i = (vecHead v • w + vecMul (vecTail v) (↑of B)) i
simp [vecMul]