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
r : k
x : V
⊢ ↑(asModuleEquiv ρ) (↑(AddEquiv.symm (asModuleEquiv ρ)) (r • x)) =
    ↑(asModuleEquiv ρ) (↑(algebraMap k (MonoidAlgebra k G)) r • ↑(AddEquiv.symm (asModuleEquiv ρ)) x)
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
r : k
x : V
⊢ ↑(AddEquiv.symm (asModuleEquiv ρ)) (r • x) =
    ↑(algebraMap k (MonoidAlgebra k G)) r • ↑(AddEquiv.symm (asModuleEquiv ρ)) x
apply_fun ρ.asModuleEquiv
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
r : k
x : V
⊢ ↑(asModuleEquiv ρ) (↑(AddEquiv.symm (asModuleEquiv ρ)) (r • x)) =
    ↑(asModuleEquiv ρ) (↑(algebraMap k (MonoidAlgebra k G)) r • ↑(AddEquiv.symm (asModuleEquiv ρ)) x)
simp