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