case h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : Semiring α
x : α
v : Fin n → α
B : Fin (Nat.succ n) → o' → α
i : o'
⊢ vecMul (vecCons x v) (↑of B) i = (x • vecHead B + vecMul v (↑of (vecTail B))) i
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : Semiring α
x : α
v : Fin n → α
B : Fin (Nat.succ n) → o' → α
⊢ vecMul (vecCons x v) (↑of B) = x • vecHead B + vecMul v (↑of (vecTail 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 α
x : α
v : Fin n → α
B : Fin (Nat.succ n) → o' → α
i : o'
⊢ vecMul (vecCons x v) (↑of B) i = (x • vecHead B + vecMul v (↑of (vecTail B))) i
simp [vecMul]