k : Type u₁
G : Type u₂
R : Type ?u.844334
inst✝¹ : CommSemiring k
inst✝ : MulOneClass G
r : k
f : MonoidAlgebra k G
x✝ : G
⊢ ↑(single 1 r * f) x✝ = ↑(f * single 1 r) x✝
k : Type u₁
G : Type u₂
R : Type ?u.844334
inst✝¹ : CommSemiring k
inst✝ : MulOneClass G
r : k
f : MonoidAlgebra k G
⊢ single 1 r * f = f * single 1 r
refine Finsupp.ext fun _ => ?_
no goals
k : Type u₁
G : Type u₂
R : Type ?u.844334
inst✝¹ : CommSemiring k
inst✝ : MulOneClass G
r : k
f : MonoidAlgebra k G
x✝ : G
⊢ ↑(single 1 r * f) x✝ = ↑(f * single 1 r) x✝
rw [single_one_mul_apply, mul_single_one_apply, mul_comm]