English
Let N be an additive commutative monoid and k a semiring with a distributive scalar action from R. For g ∈ SkewMonoidAlgebra k G, b ∈ R, h : G → k → N with h(i,0)=0 for all i, we have (b • g).sum h = g.sum (h · (b • ·)).
Русский
Пусть N — аддитивная коммутативная группа, k — полугруппа с распределяющим действием от R. Для любого g ∈ SkewMonoidAlgebra k G, b ∈ R и 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)) $ при условии $h(i,0)=0$ для всех i.$$
Lean4
theorem sum_smul_index' {N R : Type*} [AddCommMonoid k] [DistribSMul R k] [AddCommMonoid N] {g : SkewMonoidAlgebra k G}
{b : R} {h : G → k → N} (h0 : ∀ i, h i 0 = 0) : (b • g).sum h = g.sum (h · <| b • ·) := by
simp only [sum_def, toFinsupp_smul, Finsupp.sum_smul_index' h0]
