English
Let N be an additive commutative monoid and k a non-unital, non-associative semiring. For any g in the skew-monomial algebra SkewMonoidAlgebra k G, any b in k, and any h: G → k → N with h(i,0) = 0 for all i, the sum defined by h applied to the scalar-multiplied element b • g equals the sum of g applied to the shifted weight h, i.e. (b • g).sum h = g.sum (h · (b · ·)).
Русский
Пусть N — коммутативная абелева группа, k — неединичное неполностью ассоциативное полугруппа-коляско. Для любого g из SkewMonoidAlgebra k G, любого b из k и любого h: G → k → N с условием h(i,0) = 0, выполняется равенство: (b • g).sum h = g.sum (h · (b · ·)).
LaTeX
$$$ (b \cdot g).sum h = g.sum (h \cdot (b \cdot \, \cdot)) \quad\text{for all } h \text{ with } h(i,0)=0, \forall i. $$$
Lean4
theorem sum_smul_index {N : Type*} [AddCommMonoid N] [NonUnitalNonAssocSemiring k] {g : SkewMonoidAlgebra k G} {b : k}
{h : G → k → N} (h0 : ∀ i, h i 0 = 0) : (b • g).sum h = g.sum (h · <| b * ·) := by
simp [sum_def, Finsupp.sum_smul_index' h0]
/- Variant of the interaction of `sum` and `•` assuming some scalar multiplication structure. -/
