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