English
Let s be a finite set of indices and n a natural number. Then the multiset obtained by summing the finitely supported functions single i n over i in s equals n copies of the multiset s.val, i.e. Finsupp.toMultiset(∑ i∈s, single i n) = n · s.val.
Русский
Пусть s — конечное подмножество ι, и n ∈ ℕ. Тогда мультимножество, полученное суммированием одиночек single i n по i∈s, равно n копиям мультимножества s.val: Finsupp.toMultiset(∑ i∈s, single i n) = n · s.val.
LaTeX
$$$\mathrm{Finsupp.toMultiset}\left(\sum_{i \in s} \mathrm{single}(i,n)\right) = n \cdot s_{val}$$$
Lean4
theorem toMultiset_sum_single (s : Finset ι) (n : ℕ) : Finsupp.toMultiset (∑ i ∈ s, single i n) = n • s.val := by
simp_rw [toMultiset_sum, Finsupp.toMultiset_single, Finset.sum_nsmul, sum_multiset_singleton]
