k : Type u_3
G : Type u_2
V : Type ?u.513125
inst✝⁴ : CommSemiring k
inst✝³ : Group G
inst✝² : AddCommMonoid V
inst✝¹ : Module k V
ρ : Representation k G V
H : Type u_1
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
⊢ ↑(↑(↑(ofMulAction k G H) g) f) (g • g⁻¹ • h) = ↑f (g⁻¹ • h)
k : Type u_3
G : Type u_2
V : Type ?u.513125
inst✝⁴ : CommSemiring k
inst✝³ : Group G
inst✝² : AddCommMonoid V
inst✝¹ : Module k V
ρ : Representation k G V
H : Type u_1
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
⊢ ↑(↑(↑(ofMulAction k G H) g) f) h = ↑f (g⁻¹ • h)
conv_lhs => rw [← smul_inv_smul g h]
k : Type u_3
G : Type u_2
V : Type ?u.513125
inst✝⁴ : CommSemiring k
inst✝³ : Group G
inst✝² : AddCommMonoid V
inst✝¹ : Module k V
ρ : Representation k G V
H : Type u_1
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
h' : H := g⁻¹ • h
⊢ ↑(↑(↑(ofMulAction k G H) g) f) (g • g⁻¹ • h) = ↑f (g⁻¹ • h)
k : Type u_3
G : Type u_2
V : Type ?u.513125
inst✝⁴ : CommSemiring k
inst✝³ : Group G
inst✝² : AddCommMonoid V
inst✝¹ : Module k V
ρ : Representation k G V
H : Type u_1
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
⊢ ↑(↑(↑(ofMulAction k G H) g) f) (g • g⁻¹ • h) = ↑f (g⁻¹ • h)
let h' := g⁻¹ • h
k : Type u_3
G : Type u_2
V : Type ?u.513125
inst✝⁴ : CommSemiring k
inst✝³ : Group G
inst✝² : AddCommMonoid V
inst✝¹ : Module k V
ρ : Representation k G V
H : Type u_1
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
h' : H := g⁻¹ • h
⊢ ↑(↑(↑(ofMulAction k G H) g) f) (g • h') = ↑f h'
k : Type u_3
G : Type u_2
V : Type ?u.513125
inst✝⁴ : CommSemiring k
inst✝³ : Group G
inst✝² : AddCommMonoid V
inst✝¹ : Module k V
ρ : Representation k G V
H : Type u_1
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
h' : H := g⁻¹ • h
⊢ ↑(↑(↑(ofMulAction k G H) g) f) (g • g⁻¹ • h) = ↑f (g⁻¹ • h)
change ofMulAction k G H g f (g • h') = f h'
no goals
k : Type u_3
G : Type u_2
V : Type ?u.513125
inst✝⁴ : CommSemiring k
inst✝³ : Group G
inst✝² : AddCommMonoid V
inst✝¹ : Module k V
ρ : Representation k G V
H : Type u_1
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
h' : H := g⁻¹ • h
hg : Function.Injective ((fun x x_1 => x • x_1) g)
⊢ ↑(↑(↑(ofMulAction k G H) g) f) (g • h') = ↑f h'
simp only [ofMulAction_def, Finsupp.lmapDomain_apply, Finsupp.mapDomain_apply, hg]
k : Type u_3
G : Type u_2
V : Type ?u.513125
inst✝⁴ : CommSemiring k
inst✝³ : Group G
inst✝² : AddCommMonoid V
inst✝¹ : Module k V
ρ : Representation k G V
H : Type u_1
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
h' : H := g⁻¹ • h
h₁ h₂ : H
⊢ (fun x x_1 => x • x_1) g h₁ = (fun x x_1 => x • x_1) g h₂ → h₁ = h₂
k : Type u_3
G : Type u_2
V : Type ?u.513125
inst✝⁴ : CommSemiring k
inst✝³ : Group G
inst✝² : AddCommMonoid V
inst✝¹ : Module k V
ρ : Representation k G V
H : Type u_1
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
h' : H := g⁻¹ • h
⊢ Function.Injective ((fun x x_1 => x • x_1) g)
intro h₁ h₂
no goals
k : Type u_3
G : Type u_2
V : Type ?u.513125
inst✝⁴ : CommSemiring k
inst✝³ : Group G
inst✝² : AddCommMonoid V
inst✝¹ : Module k V
ρ : Representation k G V
H : Type u_1
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
h' : H := g⁻¹ • h
h₁ h₂ : H
⊢ (fun x x_1 => x • x_1) g h₁ = (fun x x_1 => x • x_1) g h₂ → h₁ = h₂
simp