case h.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix m' (Fin (Nat.succ n)) α
i : Fin n
j : m'
⊢ vecTail (↑of.symm Aᵀ) i j = (vecTail ∘ A)ᵀ i j
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix m' (Fin (Nat.succ n)) α
⊢ vecTail (↑of.symm Aᵀ) = (vecTail ∘ A)ᵀ
ext (i j)
no goals
case h.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
A : Matrix m' (Fin (Nat.succ n)) α
i : Fin n
j : m'
⊢ vecTail (↑of.symm Aᵀ) i j = (vecTail ∘ A)ᵀ i j
rfl