mathlib3 documentation

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 #

Main theorems #

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)] :
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 : ), list.nil.nthd 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_concat_eq_to_finsupp_add_single {R : Type u_1} [add_zero_class R] (x : R) (xs : list R) [decidable_pred (λ (i : ), (xs ++ [x]).nthd i 0 0)] [decidable_pred (λ (i : ), xs.nthd i 0 0)] :
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), finsupp.single nr.fst nr.snd) l.enum).sum