# `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 map `Fin (n + 1) →₀ M`, i.e., its last `n` entries;
- `Finsupp.cons` : adding an element at the beginning of an `n`-tuple, to get an `n + 1`-tuple;

In this context, we prove some usual properties of `tail` and `cons`, analogous to those of `Data.Fin.Tuple.Basic`.

source
def Finsupp.tail {n : ℕ} {M : Type u_1} [Zero M] (s : Fin (n + 1) →₀ M) :
Fin n →₀ M

`tail` for maps `Fin (n + 1) →₀ M`. See `Fin.tail` for more details.

Equations

- s.tail = Finsupp.equivFunOnFinite.symm (Fin.tail ⇑s)

Instances For

source
def Finsupp.cons {n : ℕ} {M : Type u_1} [Zero M] (y : M) (s : Fin n →₀ M) :
Fin (n + 1) →₀ M

`cons` for maps `Fin n →₀ M`. See `Fin.cons` for more details.

Equations

- Finsupp.cons y s = Finsupp.equivFunOnFinite.symm (Fin.cons y ⇑s)

Instances For

source
theorem Finsupp.tail_apply {n : ℕ} (i : Fin n) {M : Type u_1} [Zero M] (t : Fin (n + 1) →₀ M) :
t.tail i = t i.succ
source
@[simp]
theorem Finsupp.cons_zero {n : ℕ} {M : Type u_1} [Zero M] (y : M) (s : Fin n →₀ M) :
(cons y s) 0 = y
source
@[simp]
theorem Finsupp.cons_succ {n : ℕ} (i : Fin n) {M : Type u_1} [Zero M] (y : M) (s : Fin n →₀ M) :
(cons y s) i.succ = s i
source
@[simp]
theorem Finsupp.tail_cons {n : ℕ} {M : Type u_1} [Zero M] (y : M) (s : Fin n →₀ M) :
(cons y s).tail = s
source
@[simp]
theorem Finsupp.tail_update_zero {n : ℕ} {M : Type u_1} [Zero M] (y : M) (t : Fin (n + 1) →₀ M) :
(t.update 0 y).tail = t.tail
source
@[simp]
theorem Finsupp.tail_update_succ {n : ℕ} (i : Fin n) {M : Type u_1} [Zero M] (y : M) (t : Fin (n + 1) →₀ M) :
(t.update i.succ y).tail = t.tail.update i y
source
@[simp]
theorem Finsupp.cons_tail {n : ℕ} {M : Type u_1} [Zero M] (t : Fin (n + 1) →₀ M) :
cons (t 0) t.tail = t
source
@[simp]
theorem Finsupp.cons_zero_zero {n : ℕ} {M : Type u_1} [Zero M] :
cons 0 0 = 0
source
theorem Finsupp.cons_ne_zero_of_left {n : ℕ} {M : Type u_1} [Zero M] {y : M} {s : Fin n →₀ M} (h : y ≠ 0) :
cons y s ≠ 0
source
theorem Finsupp.cons_ne_zero_of_right {n : ℕ} {M : Type u_1} [Zero M] {y : M} {s : Fin n →₀ M} (h : s ≠ 0) :
cons y s ≠ 0
source
theorem Finsupp.cons_ne_zero_iff {n : ℕ} {M : Type u_1} [Zero M] {y : M} {s : Fin n →₀ M} :
cons y s ≠ 0 ↔ y ≠ 0 ∨ s ≠ 0
source
theorem Finsupp.cons_support {n : ℕ} {M : Type u_1} [Zero M] {y : M} {s : Fin n →₀ M} :
(cons y s).support ⊆ insert 0 (Finset.map (Fin.succEmb n) s.support)
source
theorem Finsupp.cons_right_injective {n : ℕ} {M : Type u_2} [Zero M] (y : M) :
Function.Injective (cons y)