English
The toFinsupp of a list equals the sum over elements with their indices mapped to singletons.
Русский
ToFinsupp списка равен сумме по элементам с индексами, отображёнными в одинокие значения.
LaTeX
$$$$ \\operatorname{toFinsupp} l = (l.\\operatorname{mapIdx} (\\lambda n r \\; \\Rightarrow \\mathsf{single}\\, n\\, r)).\\text{sum} $$$$
Lean4
theorem toFinsupp_eq_sum_mapIdx_single {R : Type*} [AddMonoid R] (l : List R) [DecidablePred (getD l · 0 ≠ 0)] :
toFinsupp l = (l.mapIdx fun n r => Finsupp.single n r).sum := by
/- Porting note: `induction` fails to substitute `l = []` in
`[DecidablePred (getD l · 0 ≠ 0)]`, so we manually do some `revert`/`intro` as a workaround -/
revert l; intro l
induction l using List.reverseRecOn with
| nil => exact toFinsupp_nil
| append_singleton x xs ih => classical simp [toFinsupp_concat_eq_toFinsupp_add_single, ih]
