English
There is a canonical IsScalarTower structure on R, k, and MonoidAlgebra k G, i.e., the scalar action is coherent with the algebra multiplication.
Русский
Существует каноническое свойство IsScalarTower для R, k и MonoidAlgebra k G: действие скаляра согласуется с умножением в алгебре.
LaTeX
$$$$IsScalarTower\ R\ (k)\ (k[G]).$$$$
Lean4
instance isScalarTower_self [IsScalarTower R k k] : IsScalarTower R (MonoidAlgebra k G) (MonoidAlgebra k G) where
smul_assoc 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.trans (sum_smul_index' (g := a) (b := t) ?_) ?_ <;>
simp only [mul_apply, Finsupp.smul_sum, smul_ite, smul_mul_assoc, zero_mul, ite_self, imp_true_iff, sum_zero,
Pi.smul_apply, smul_zero]
