case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : Semiring α
x : α
v : Fin m → α
w : n' → α
i : Fin (Nat.succ m)
x✝ : n'
⊢ vecMulVec (vecCons x v) w i x✝ = vecCons (x • w) (vecMulVec v w) i x✝
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : Semiring α
x : α
v : Fin m → α
w : n' → α
⊢ vecMulVec (vecCons x v) w = vecCons (x • w) (vecMulVec v w)
ext i
no goals
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝ : Semiring α
x : α
v : Fin m → α
w : n' → α
i : Fin (Nat.succ m)
x✝ : n'
⊢ vecMulVec (vecCons x v) w i x✝ = vecCons (x • w) (vecMulVec v w) i x✝
refine' Fin.cases _ _ i <;> simp [vecMulVec]