sum_toFinset_count_eq_length — Mathlib

English

For any list l, the sum over a ∈ l.toFinset of l.count a equals the length of l: ∑ a ∈ l.toFinset, l.count a = length(l).

Русский

Для любого списка l сумма по всем элементам из l.toFinset их кратностей равна размеру списка: ∑ a ∈ l.toFinset, l.count a = length(l).

LaTeX

$$$$ \\sum_{a \\in l^{\\mathrm{toFinset}}} l.count(a) = |l| $$$$

Lean4

@[simp]
theorem sum_toFinset_count_eq_length [DecidableEq ι] (l : List ι) : ∑ a ∈ l.toFinset, l.count a = l.length := by
  simpa [List.map_const'] using (Finset.sum_list_map_count l fun _ => (1 : ℕ)).symm

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