# mathlib3documentation

data.list.to_finsupp

# Lists as finsupp #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

# Main definitions #

• list.to_finsupp: Interpret a list as a finitely supported function, where the indexing type is ℕ, and the values are either the elements of the list (accessing by indexing) or 0 outside of the list.

# Main theorems #

• list.to_finsupp_eq_sum_map_enum_single: A l : list M over M an add_monoid, when interpreted as a finitely supported function, is equal to the sum of finsupp.single produced by mapping over list.enum l.

## Implementation details #

The functions defined here rely on a decidability predicate that each element in the list can be decidably determined to be not equal to zero or that one can decide one is out of the bounds of a list. For concretely defined lists that are made up of elements of decidable terms, this holds. More work will be needed to support lists over non-dec-eq types like ℝ, where the elements are beyond the dec-eq terms of casted values from ℕ, ℤ, ℚ.

def list.to_finsupp {M : Type u_1} [has_zero M] (l : list M) [decidable_pred (λ (i : ), l.nthd i 0 0)] :

Indexing into a l : list M, as a finitely-supported function, where the support are all the indices within the length of the list that index to a non-zero value. Indices beyond the end of the list are sent to 0.

This is a computable version of the finsupp.on_finset construction.

Equations
@[norm_cast]
theorem list.coe_to_finsupp {M : Type u_1} [has_zero M] (l : list M) [decidable_pred (λ (i : ), l.nthd i 0 0)] :
(l.to_finsupp) = λ (i : ), l.nthd i 0
@[simp, norm_cast]
theorem list.to_finsupp_apply {M : Type u_1} [has_zero M] (l : list M) [decidable_pred (λ (i : ), l.nthd i 0 0)] (i : ) :
(l.to_finsupp) i = l.nthd i 0
theorem list.to_finsupp_support {M : Type u_1} [has_zero M] (l : list M) [decidable_pred (λ (i : ), l.nthd i 0 0)] :
l.to_finsupp.support = finset.filter (λ (i : ), l.nthd i 0 0)
theorem list.to_finsupp_apply_lt {M : Type u_1} [has_zero M] (l : list M) [decidable_pred (λ (i : ), l.nthd i 0 0)] (n : ) (hn : n < l.length) :
(l.to_finsupp) n = l.nth_le n hn
theorem list.to_finsupp_apply_le {M : Type u_1} [has_zero M] (l : list M) [decidable_pred (λ (i : ), l.nthd i 0 0)] (n : ) (hn : l.length n) :
@[simp]
theorem list.to_finsupp_nil {M : Type u_1} [has_zero M] [decidable_pred (λ (i : ), 0 0)] :
theorem list.to_finsupp_singleton {M : Type u_1} [has_zero M] (x : M) [decidable_pred (λ (i : ), [x].nthd i 0 0)] :
@[simp]
theorem list.to_finsupp_cons_apply_zero {M : Type u_1} [has_zero M] (x : M) (xs : list M) [decidable_pred (λ (i : ), (x :: xs).nthd i 0 0)] :
((x :: xs).to_finsupp) 0 = x
@[simp]
theorem list.to_finsupp_cons_apply_succ {M : Type u_1} [has_zero M] (x : M) (xs : list M) (n : ) [decidable_pred (λ (i : ), (x :: xs).nthd i 0 0)] [decidable_pred (λ (i : ), xs.nthd i 0 0)] :
((x :: xs).to_finsupp) n.succ = (xs.to_finsupp) n
theorem list.to_finsupp_cons_eq_single_add_emb_domain {R : Type u_1} (x : R) (xs : list R) [decidable_pred (λ (i : ), (x :: xs).nthd i 0 0)] [decidable_pred (λ (i : ), xs.nthd i 0 0)] :
(x :: xs).to_finsupp = +
theorem list.to_finsupp_concat_eq_to_finsupp_add_single {R : Type u_1} (x : R) (xs : list R) [decidable_pred (λ (i : ), (xs ++ [x]).nthd i 0 0)] [decidable_pred (λ (i : ), xs.nthd i 0 0)] :
(xs ++ [x]).to_finsupp = xs.to_finsupp + x
theorem list.to_finsupp_eq_sum_map_enum_single {R : Type u_1} [add_monoid R] (l : list R) [decidable_pred (λ (i : ), l.nthd i 0 0)] :
l.to_finsupp = (list.map (λ (nr : × R), nr.snd) l.enum).sum