single_finset_sum — Mathlib

English

For any Finite-indexed family s, a, the identity with single distributes over the Finset-sum: single a (sum over s of f(b)) equals sum over s of single a (f(b)).

Русский

Для любой конечной семьи s, одинокий элемент a распределяется над суммой по Finset: single a (∑ f) = ∑ single a (f).

LaTeX

$$$$ \\mathrm{single}_a(\\sum_{b \\in S} f(b)) = \\sum_{b \\in S} \\mathrm{single}_a(f(b)) $$$$

Lean4

theorem single_finset_sum [AddCommMonoid M] (s : Finset ι) (f : ι → M) (a : α) :
    single a (∑ b ∈ s, f b) = ∑ b ∈ s, single a (f b) := by
  trans
  · apply single_multiset_sum
  · rw [Multiset.map_map]
    rfl

Похожие утверждения