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