k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
r : MonoidAlgebra k G
x : V
y : W
⊢ ↑(↑(asAlgebraHom (ρV ⊗ 1)) r) (x ⊗ₜ[k] y) = ↑(↑(asAlgebraHom ρV) r) x ⊗ₜ[k] y
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
r : MonoidAlgebra k G
x : V
y : W
⊢ let x' := x;
  let z := x ⊗ₜ[k] y;
  r • z = (r • x') ⊗ₜ[k] y
show asAlgebraHom (ρV ⊗ 1) _ _ = asAlgebraHom ρV _ _ ⊗ₜ _
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
r : MonoidAlgebra k G
x : V
y : W
⊢ (Finsupp.sum r fun i d => d • ↑(↑ρV i) x ⊗ₜ[k] y) = (Finsupp.sum r fun i d => d • ↑(↑ρV i) x) ⊗ₜ[k] y
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
r : MonoidAlgebra k G
x : V
y : W
⊢ ↑(↑(asAlgebraHom (ρV ⊗ 1)) r) (x ⊗ₜ[k] y) = ↑(↑(asAlgebraHom ρV) r) x ⊗ₜ[k] y
simp only [asAlgebraHom_def, MonoidAlgebra.lift_apply, tprod_apply, MonoidHom.one_apply,
  LinearMap.finsupp_sum_apply, LinearMap.smul_apply, TensorProduct.map_tmul, LinearMap.one_apply]
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
r : MonoidAlgebra k G
x : V
y : W
⊢ (Finset.sum r.support fun x_1 => ↑r x_1 • ↑(↑ρV x_1) x ⊗ₜ[k] y) =
    Finset.sum r.support fun a => (↑r a • ↑(↑ρV a) x) ⊗ₜ[k] y
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
r : MonoidAlgebra k G
x : V
y : W
⊢ (Finsupp.sum r fun i d => d • ↑(↑ρV i) x ⊗ₜ[k] y) = (Finsupp.sum r fun i d => d • ↑(↑ρV i) x) ⊗ₜ[k] y
simp only [Finsupp.sum, TensorProduct.sum_tmul]
no goals
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
r : MonoidAlgebra k G
x : V
y : W
⊢ (Finset.sum r.support fun x_1 => ↑r x_1 • ↑(↑ρV x_1) x ⊗ₜ[k] y) =
    Finset.sum r.support fun a => (↑r a • ↑(↑ρV a) x) ⊗ₜ[k] y
rfl