toFinset_sum_count_nsmul_eq — Mathlib

English

For any s ∈ Multiset ι, the sum over a ∈ s.toFinset of count(a, s) times {a} equals s.

Русский

Для мультсета s ∈ ι произведение суммы по a ∈ s.toFinset: count(a,s) умножить на {a} равно s.

LaTeX

$$$$ \\sum_{a \\in s^{\\mathrm{toFinset}}} \\mathrm{count}(a,s) \\;\\cdot\\; \\{a\\} = s $$$$

Lean4

@[simp]
theorem toFinset_sum_count_nsmul_eq (s : Multiset ι) : ∑ a ∈ s.toFinset, s.count a • { a } = s := by
  rw [← Finset.sum_multiset_map_count, Multiset.sum_map_singleton]

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