English
There is a Fubini-type law for Skew Monoid Algebra sums: summing over a first inner sum and then applying h equals summing over a first with an inner sum over g a b.
Русский
Существует закон Фубини для сумм в Skew Monoid Algebra: суммирование по одной и последующей функции эквивалентно суммированию в другом порядке со вложенными суммами.
LaTeX
$$$$ \mathrm{sum}(\mathrm{sum}\ f\ g)\ h = \mathrm{sum}\ f (\\lambda a b \,\\mapsto \\mathrm{sum} (g\ a\ b)\ h) $$$$
Lean4
theorem sum_sum_index {α β M N P : Type*} [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P]
{f : SkewMonoidAlgebra M α} {g : α → M → SkewMonoidAlgebra N β} {h : β → N → P} (h_zero : ∀ (a : β), h a 0 = 0)
(h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ + h a b₂) :
sum (sum f g) h = sum f fun a b ↦ sum (g a b) h := by
rw [sum_def, toFinsupp_sum' f g, Finsupp.sum_sum_index h_zero h_add]; simp [sum_def]
