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