case a.h
l : Type ?u.928988
m : Type u_1
n : Type u_2
o : Type ?u.928997
m' : o → Type ?u.929002
n' : o → Type ?u.929007
R : Type ?u.929010
S : Type ?u.929013
α : Type v
β : Type w
γ : Type ?u.929020
inst✝ : Neg α
M : Matrix m n α
i✝ : n
x✝ : m
⊢ (-M)ᵀ i✝ x✝ = (-Mᵀ) i✝ x✝
l : Type ?u.928988
m : Type u_1
n : Type u_2
o : Type ?u.928997
m' : o → Type ?u.929002
n' : o → Type ?u.929007
R : Type ?u.929010
S : Type ?u.929013
α : Type v
β : Type w
γ : Type ?u.929020
inst✝ : Neg α
M : Matrix m n α
⊢ (-M)ᵀ = -Mᵀ
ext
no goals
case a.h
l : Type ?u.928988
m : Type u_1
n : Type u_2
o : Type ?u.928997
m' : o → Type ?u.929002
n' : o → Type ?u.929007
R : Type ?u.929010
S : Type ?u.929013
α : Type v
β : Type w
γ : Type ?u.929020
inst✝ : Neg α
M : Matrix m n α
i✝ : n
x✝ : m
⊢ (-M)ᵀ i✝ x✝ = (-Mᵀ) i✝ x✝
rfl