toFinsupp_sum_eq — Mathlib

English

For s : Multiset α, the sum of the identity function over s.toFinsupp equals the cardinality of s: s.toFinsupp.sum(id) = card s.

Русский

Для s : Multiset α сумма единичной функции по s.toFinsupp равна мощности s: s.toFinsupp.sum(id) = card s.

LaTeX

$$$\mathrm{toFinsupp}(s).\sum(\mathrm{id}) = \lvert s \rvert$$$

Lean4

@[simp]
theorem toFinsupp_sum_eq (s : Multiset α) : s.toFinsupp.sum (fun _ ↦ id) = Multiset.card s := by
  rw [← Finsupp.card_toMultiset, toFinsupp_toMultiset]

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