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}
[Zero M]
(y : M)
(s : Fin n →₀ M)
:
(Finsupp.cons y s) 0 = y
@[simp]
theorem
Finsupp.cons_succ
{n : ℕ}
(i : Fin n)
{M : Type u_1}
[Zero M]
(y : M)
(s : Fin n →₀ M)
:
(Finsupp.cons y s) i.succ = s i
@[simp]
theorem
Finsupp.tail_cons
{n : ℕ}
{M : Type u_1}
[Zero M]
(y : M)
(s : Fin n →₀ M)
:
(Finsupp.cons y s).tail = s
@[simp]
theorem
Finsupp.cons_tail
{n : ℕ}
{M : Type u_1}
[Zero M]
(t : Fin (n + 1) →₀ M)
:
Finsupp.cons (t 0) t.tail = t
theorem
Finsupp.cons_ne_zero_of_left
{n : ℕ}
{M : Type u_1}
[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}
[Zero M]
{y : M}
{s : Fin n →₀ M}
(h : s ≠ 0)
:
Finsupp.cons y s ≠ 0
theorem
Finsupp.cons_support
{n : ℕ}
{M : Type u_1}
[Zero M]
{y : M}
{s : Fin n →₀ M}
:
(Finsupp.cons y s).support ⊆ insert 0 (Finset.map (Fin.succEmb n) s.support)