no goals
R : Type u_1
inst✝² : CommSemiring R
k : Type ?u.932592
l : Type ?u.932595
m : Type ?u.932598
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
x : R
⊢ ↑toMatrix' (↑(algebraMap R (Module.End R (n → R))) x) = ↑(scalar n) x
simp [Module.algebraMap_end_eq_smul_id]