case a.h
l : Type ?u.928657
m : Type u_2
n : Type u_3
o : Type ?u.928666
m' : o → Type ?u.928671
n' : o → Type ?u.928676
R✝ : Type ?u.928679
S : Type ?u.928682
α : Type v
β : Type w
γ : Type ?u.928689
R : Type u_1
inst✝ : SMul R α
c : R
M : Matrix m n α
i✝ : n
x✝ : m
⊢ (c • M)ᵀ i✝ x✝ = (c • Mᵀ) i✝ x✝
l : Type ?u.928657
m : Type u_2
n : Type u_3
o : Type ?u.928666
m' : o → Type ?u.928671
n' : o → Type ?u.928676
R✝ : Type ?u.928679
S : Type ?u.928682
α : Type v
β : Type w
γ : Type ?u.928689
R : Type u_1
inst✝ : SMul R α
c : R
M : Matrix m n α
⊢ (c • M)ᵀ = c • Mᵀ
ext
no goals
case a.h
l : Type ?u.928657
m : Type u_2
n : Type u_3
o : Type ?u.928666
m' : o → Type ?u.928671
n' : o → Type ?u.928676
R✝ : Type ?u.928679
S : Type ?u.928682
α : Type v
β : Type w
γ : Type ?u.928689
R : Type u_1
inst✝ : SMul R α
c : R
M : Matrix m n α
i✝ : n
x✝ : m
⊢ (c • M)ᵀ i✝ x✝ = (c • Mᵀ) i✝ x✝
rfl