k : Type u_1
G : Type u_2
V : Type ?u.568789
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x : MonoidAlgebra k G
y : asModule (ofMulAction k G G)
g : G
⊢ ↑(↑(asAlgebraHom (ofMulAction k G G)) (↑(of k G) g)) y = ↑(of k G) g * y
k : Type u_1
G : Type u_2
V : Type ?u.568789
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x : MonoidAlgebra k G
y : asModule (ofMulAction k G G)
g : G
⊢ (fun z => z • y = z * y) (↑(of k G) g)
show asAlgebraHom (ofMulAction k G G) _ _ = _
case h
k : Type u_1
G : Type u_2
V : Type ?u.568789
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x : MonoidAlgebra k G
y : asModule (ofMulAction k G G)
g a✝ : G
⊢ ↑(↑(↑(asAlgebraHom (ofMulAction k G G)) (↑(of k G) g)) y) a✝ = ↑(↑(of k G) g * y) a✝
k : Type u_1
G : Type u_2
V : Type ?u.568789
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x : MonoidAlgebra k G
y : asModule (ofMulAction k G G)
g : G
⊢ ↑(↑(asAlgebraHom (ofMulAction k G G)) (↑(of k G) g)) y = ↑(of k G) g * y
ext
case h
k : Type u_1
G : Type u_2
V : Type ?u.568789
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x : MonoidAlgebra k G
y : asModule (ofMulAction k G G)
g a✝ : G
⊢ ↑y (g⁻¹ * a✝) = ↑(MonoidAlgebra.single g 1 * y) a✝
case h
k : Type u_1
G : Type u_2
V : Type ?u.568789
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x : MonoidAlgebra k G
y : asModule (ofMulAction k G G)
g a✝ : G
⊢ ↑(↑(↑(asAlgebraHom (ofMulAction k G G)) (↑(of k G) g)) y) a✝ = ↑(↑(of k G) g * y) a✝
simp only [MonoidAlgebra.of_apply, asAlgebraHom_single, one_smul,
  ofMulAction_apply, smul_eq_mul]
no goals
case h
k : Type u_1
G : Type u_2
V : Type ?u.568789
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x : MonoidAlgebra k G
y : asModule (ofMulAction k G G)
g a✝ : G
⊢ ↑y (g⁻¹ * a✝) = ↑(MonoidAlgebra.single g 1 * y) a✝
rw [MonoidAlgebra.single_mul_apply, one_mul]
no goals
k : Type u_1
G : Type u_2
V : Type ?u.568789
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x✝ : MonoidAlgebra k G
y✝ : asModule (ofMulAction k G G)
x y : MonoidAlgebra k G
hx : (fun z => z • y✝ = z * y✝) x
hy : (fun z => z • y✝ = z * y✝) y
⊢ (fun z => z • y✝ = z * y✝) (x + y)
simp only [hx, hy, add_mul, add_smul]
k : Type u_1
G : Type u_2
V : Type ?u.568789
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x✝ : MonoidAlgebra k G
y : asModule (ofMulAction k G G)
r : k
x : MonoidAlgebra k G
hx : (fun z => z • y = z * y) x
⊢ ↑(↑(asAlgebraHom (ofMulAction k G G)) (r • x)) y = r • x * y
k : Type u_1
G : Type u_2
V : Type ?u.568789
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x✝ : MonoidAlgebra k G
y : asModule (ofMulAction k G G)
r : k
x : MonoidAlgebra k G
hx : (fun z => z • y = z * y) x
⊢ (fun z => z • y = z * y) (r • x)
show asAlgebraHom (ofMulAction k G G) _ _ = _
k : Type u_1
G : Type u_2
V : Type ?u.568789
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x✝ : MonoidAlgebra k G
y : asModule (ofMulAction k G G)
r : k
x : MonoidAlgebra k G
hx : (fun z => z • y = z * y) x
⊢ r • ↑(↑(asAlgebraHom (ofMulAction k G G)) x) y = r • (x * y)
k : Type u_1
G : Type u_2
V : Type ?u.568789
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x✝ : MonoidAlgebra k G
y : asModule (ofMulAction k G G)
r : k
x : MonoidAlgebra k G
hx : (fun z => z • y = z * y) x
⊢ ↑(↑(asAlgebraHom (ofMulAction k G G)) (r • x)) y = r • x * y
simp only [map_smul, smul_apply, Algebra.smul_mul_assoc]
k : Type u_1
G : Type u_2
V : Type ?u.568789
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x✝ : MonoidAlgebra k G
y : asModule (ofMulAction k G G)
r : k
x : MonoidAlgebra k G
hx : (fun z => z • y = z * y) x
⊢ r • ↑(↑(asAlgebraHom (ofMulAction k G G)) x) y = r • x • y
k : Type u_1
G : Type u_2
V : Type ?u.568789
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x✝ : MonoidAlgebra k G
y : asModule (ofMulAction k G G)
r : k
x : MonoidAlgebra k G
hx : (fun z => z • y = z * y) x
⊢ r • ↑(↑(asAlgebraHom (ofMulAction k G G)) x) y = r • (x * y)
rw [←hx]
no goals
k : Type u_1
G : Type u_2
V : Type ?u.568789
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x✝ : MonoidAlgebra k G
y : asModule (ofMulAction k G G)
r : k
x : MonoidAlgebra k G
hx : (fun z => z • y = z * y) x
⊢ r • ↑(↑(asAlgebraHom (ofMulAction k G G)) x) y = r • x • y
rfl