no goals
l : Type ?u.445575
m : Type ?u.445578
n : Type u_1
o : Type ?u.445584
m' : o → Type ?u.445589
n' : o → Type ?u.445594
R : Type ?u.445597
S : Type ?u.445600
α : Type v
β : Type w
γ : Type ?u.445607
inst✝² : Semiring α
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a : α
i j : n
h : i ≠ j
⊢ ↑(scalar n) a i j = 0
simp only [h, coe_scalar, one_apply_ne, Ne.def, not_false_iff, Matrix.smul_apply, smul_zero]