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