no goals
k : Type u_2
G : Type u_3
V : Type u_1
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
⊢ ↑(asAlgebraHom ρ) (Finsupp.single g 1) = ↑ρ g
simp