no goals
l : Type ?u.45650
m : Type ?u.45653
n : Type u_1
o : Type ?u.45659
m' : o → Type ?u.45664
n' : o → Type ?u.45669
R : Type ?u.45672
S : Type ?u.45675
α : Type v
β : Type w
γ : Type ?u.45682
inst✝¹ : DecidableEq n
inst✝ : Zero α
d : n → α
i j : n
h : i ≠ j
⊢ diagonal d i j = 0
simp [diagonal, h]