no goals
l : Type ?u.432380
m : Type ?u.432383
n : Type u_1
o : Type ?u.432389
m' : o → Type ?u.432394
n' : o → Type ?u.432399
R : Type ?u.432402
S : Type ?u.432405
α : Type v
β : Type w
γ : Type ?u.432412
inst✝² : Semiring α
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a : α
i : n
⊢ ↑(scalar n) a i i = a
simp only [coe_scalar, Matrix.smul_apply, one_apply_eq, smul_eq_mul, mul_one]