English
If k is a semiring and R acts on k with a commuting action, then the induced action on MonoidAlgebra k G also commutes with its internal multiplication.
Русский
Если k — полупрямой полугруппа и R действия на k коммутирует, то и действие на MonoidAlgebra k G коммутирует с внутренним умножением.
LaTeX
$$$$\text{SMulCommClass } R (k[G]) (k[G]).$$$$
Lean4
/-- Note that if `k` is a `CommSemiring` then we have `SMulCommClass k k k` and so we can take
`R = k` in the below. In other words, if the coefficients are commutative amongst themselves, they
also commute with the algebra multiplication. -/
instance smulCommClass_self [SMulCommClass R k k] : SMulCommClass R (MonoidAlgebra k G) (MonoidAlgebra k G) where
smul_comm t a
b :=
by
ext
-- Porting note: `refine` & `rw` are required because `simp` behaves differently.
classical
simp only [smul_eq_mul, mul_apply]
rw [coe_smul]
refine Eq.symm (Eq.trans (congr_arg (sum a) (funext₂ fun a₁ b₁ => sum_smul_index' (g := b) (b := t) ?_)) ?_) <;>
simp only [mul_apply, Finsupp.sum, Finset.smul_sum, smul_ite, mul_smul_comm, imp_true_iff, ite_eq_right_iff,
Pi.smul_apply, mul_zero, smul_zero]
