case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
v : n' → α
A : Matrix (Fin m) n' α
i : n'
j : Fin (Nat.succ m)
⊢ (↑of (vecCons v A))ᵀ i j = ↑of (fun i => vecCons (v i) (Aᵀ i)) i j
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
v : n' → α
A : Matrix (Fin m) n' α
⊢ (↑of (vecCons v A))ᵀ = ↑of fun i => vecCons (v i) (Aᵀ i)
ext (i j)
no goals
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
v : n' → α
A : Matrix (Fin m) n' α
i : n'
j : Fin (Nat.succ m)
⊢ (↑of (vecCons v A))ᵀ i j = ↑of (fun i => vecCons (v i) (Aᵀ i)) i j
refine' Fin.cases _ _ j <;> simp