English
Let f : α → β, s : α →₀ M and h : β → M →+ N with N an AddCommMonoid. Then the Finset-sum over the domain after applying mapDomain to s, using the function (b, m) ↦ h b m, equals the sum over the original domain of s with the argument mapped by f, i.e. (mapDomain f s).sum (λ b m, h b m) = s.sum (λ a m, h (f a) m).
Русский
Пусть f : α → β, s : α →₀ M и h : β → M →+ N, где N – коммутативное моноидоидное. Тогда сумма по диапазону после применения mapDomain к s, с функцией (b, m) ↦ h b m, равна сумме по исходному диапазону s, при этом аргумент f(a) используется вместо a: (mapDomain f s).sum (λ b m, h b m) = s.sum (λ a m, h (f a) m).
LaTeX
$$$$ (mapDomain\ f\ s).sum (\lambda b\, m,\; h\ b\ m) = s.sum (\lambda a\, m,\; h\ (f\ a)\ m). $$$$
Lean4
/-- A version of `sum_mapDomain_index` that takes a bundled `AddMonoidHom`,
rather than separate linearity hypotheses.
-/
@[simp]
theorem sum_mapDomain_index_addMonoidHom [AddCommMonoid N] {f : α → β} {s : α →₀ M} (h : β → M →+ N) :
((mapDomain f s).sum fun b m => h b m) = s.sum fun a m => h (f a) m :=
sum_mapDomain_index (fun b => (h b).map_zero) (fun b _ _ => (h b).map_add _ _)
