no goals
k : Type u₁
G : Type u₂
R : Type ?u.1513482
inst✝¹ : Semiring k
inst✝ : Group G
f g : MonoidAlgebra k G
x : G
⊢ ↑(f * g) x = sum f fun a b => ↑(single a b * g) x
rw [← Finsupp.sum_apply, ← Finsupp.sum_mul g f, f.sum_single]
no goals
k : Type u₁
G : Type u₂
R : Type ?u.1513482
inst✝¹ : Semiring k
inst✝ : Group G
f g : MonoidAlgebra k G
x : G
⊢ (sum f fun a b => ↑(single a b * g) x) = sum f fun a b => b * ↑g (a⁻¹ * x)
simp only [single_mul_apply, Finsupp.sum]