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