case a.h
l : Type u_4
m : Type u_3
n : Type u_1
o : Type ?u.251620
m' : o → Type ?u.251625
n' : o → Type ?u.251630
R : Type u_2
S : Type ?u.251636
α : Type v
β : Type w
γ : Type ?u.251643
inst✝⁵ : AddCommMonoid α
inst✝⁴ : Mul α
inst✝³ : Fintype n
inst✝² : Monoid R
inst✝¹ : DistribMulAction R α
inst✝ : IsScalarTower R α α
a : R
M : Matrix m n α
N : Matrix n l α
i✝ : m
x✝ : l
⊢ ((a • M) ⬝ N) i✝ x✝ = (a • M ⬝ N) i✝ x✝
l : Type u_4
m : Type u_3
n : Type u_1
o : Type ?u.251620
m' : o → Type ?u.251625
n' : o → Type ?u.251630
R : Type u_2
S : Type ?u.251636
α : Type v
β : Type w
γ : Type ?u.251643
inst✝⁵ : AddCommMonoid α
inst✝⁴ : Mul α
inst✝³ : Fintype n
inst✝² : Monoid R
inst✝¹ : DistribMulAction R α
inst✝ : IsScalarTower R α α
a : R
M : Matrix m n α
N : Matrix n l α
⊢ (a • M) ⬝ N = a • M ⬝ N
ext
no goals
case a.h
l : Type u_4
m : Type u_3
n : Type u_1
o : Type ?u.251620
m' : o → Type ?u.251625
n' : o → Type ?u.251630
R : Type u_2
S : Type ?u.251636
α : Type v
β : Type w
γ : Type ?u.251643
inst✝⁵ : AddCommMonoid α
inst✝⁴ : Mul α
inst✝³ : Fintype n
inst✝² : Monoid R
inst✝¹ : DistribMulAction R α
inst✝ : IsScalarTower R α α
a : R
M : Matrix m n α
N : Matrix n l α
i✝ : m
x✝ : l
⊢ ((a • M) ⬝ N) i✝ x✝ = (a • M ⬝ N) i✝ x✝
apply smul_dotProduct