English
For f: α →₀ β →₀ M and g: α × β → M → N, the identity f.uncurry.sum (λ p c, g p c) equals f.sum (λ a f, f.sum (λ b, g (a,b))).
Русский
Для f: α →₀ β →₀ M и g: α×β → M→N выполняется равенство: f.uncurry.sum (λ p c, g p c) = f.sum (λ a f, f.sum (λ b, g (a,b))).
LaTeX
$$$f.uncurry.sum(\lambda p\, c.\, g\,p\,c) = f.sum(\lambda a\, f.\, f.sum(\lambda b.\, g (a,b)))$$$
Lean4
theorem sum_uncurry_index [AddCommMonoid N] (f : α →₀ β →₀ M) (g : α × β → M → N) :
f.uncurry.sum (fun p c => g p c) = f.sum fun a f => f.sum fun b ↦ g (a, b) := by
simp [Finsupp.sum, Finsupp.uncurry, Finset.sum_disjiUnion]