case h
α✝ : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Semiring α✝
α : Type u_1
inst✝ : CommSemiring α
A : m' → Fin (Nat.succ n) → α
x : α
v : Fin n → α
i : m'
⊢ mulVec (↑of A) (vecCons x v) i = (x • vecHead ∘ A + mulVec (↑of (vecTail ∘ A)) v) i
α✝ : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Semiring α✝
α : Type u_1
inst✝ : CommSemiring α
A : m' → Fin (Nat.succ n) → α
x : α
v : Fin n → α
⊢ mulVec (↑of A) (vecCons x v) = x • vecHead ∘ A + mulVec (↑of (vecTail ∘ A)) v
ext i
no goals
case h
α✝ : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
inst✝¹ : Semiring α✝
α : Type u_1
inst✝ : CommSemiring α
A : m' → Fin (Nat.succ n) → α
x : α
v : Fin n → α
i : m'
⊢ mulVec (↑of A) (vecCons x v) i = (x • vecHead ∘ A + mulVec (↑of (vecTail ∘ A)) v) i
simp [mulVec, mul_comm]