cons and tail for maps fin n →₀ M #
We interpret maps fin n →₀ M as n-tuples of elements of M,
We define the following operations:
finsupp.tail: the tail of a mapfin (n + 1) →₀ M, i.e., its lastnentries;finsupp.cons: adding an element at the beginning of ann-tuple, to get ann + 1-tuple;
In this context, we prove some usual properties of tail and cons, analogous to those of
data.fin.tuple.basic.
@[simp]
theorem
finsupp.cons_zero
{n : ℕ}
{M : Type u_1}
[has_zero M]
(y : M)
(s : fin n →₀ M) :
⇑(finsupp.cons y s) 0 = y
@[simp]
theorem
finsupp.tail_cons
{n : ℕ}
{M : Type u_1}
[has_zero M]
(y : M)
(s : fin n →₀ M) :
(finsupp.cons y s).tail = s
@[simp]
theorem
finsupp.cons_ne_zero_of_left
{n : ℕ}
{M : Type u_1}
[has_zero M]
{y : M}
{s : fin n →₀ M}
(h : y ≠ 0) :
finsupp.cons y s ≠ 0
theorem
finsupp.cons_ne_zero_of_right
{n : ℕ}
{M : Type u_1}
[has_zero M]
{y : M}
{s : fin n →₀ M}
(h : s ≠ 0) :
finsupp.cons y s ≠ 0