no goals
l : Type ?u.34238
m : Type ?u.34241
n : Type u_1
R : Type ?u.34247
α : Type u_2
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
a : n
M : Matrix n n α
⊢ (M ⬝ stdBasisMatrix i j c) a j = M a i * c
simp [mul_apply, stdBasisMatrix, mul_comm]