no goals
l : Type ?u.29224
m : Type ?u.29227
n : Type u_2
R : Type ?u.29233
α : Type u_1
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
⊢ trace (stdBasisMatrix i i c) = c
simp [trace, -diag_apply]