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.

noncomputable 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)

noncomputable 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)

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

@[simp]

theorem Finsupp.cons_zero {n : ℕ} {M : Type u_1} [Zero M] (y : M) (s : Fin n →₀ M) : (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) : (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) : (cons y s).tail = s

@[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

@[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

@[simp]

theorem Finsupp.cons_tail {n : ℕ} {M : Type u_1} [Zero M] (t : Fin (n + 1) →₀ M) : cons (t 0) t.tail = t

theorem Finsupp.cons_zero_eq_single_zero {n : ℕ} {M : Type u_1} [Zero M] (y : M) : cons y 0 = single 0 y

theorem Finsupp.cons_zero_single_eq_single_succ {n : ℕ} (i : Fin n) {M : Type u_1} [Zero M] (y : M) : cons 0 (single i y) = single i.succ y

@[simp]

theorem Finsupp.cons_zero_zero {n : ℕ} {M : Type u_1} [Zero M] : cons 0 0 = 0

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

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

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

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)

theorem Finsupp.cons_right_injective {n : ℕ} {M : Type u_1} [Zero M] (y : M) : Function.Injective (cons y)

theorem Finsupp.cons_injective2 {n : ℕ} {M : Type u_1} [Zero M] : Function.Injective2 cons

As a binary function, Finsupp.cons is injective.

theorem Finsupp.cons_eq_single_zero_iff {n : ℕ} {M : Type u_1} [Zero M] {y : M} {s : Fin n →₀ M} {x : M} : cons x s = single 0 y ↔ s = 0 ∧ x = y

theorem Finsupp.cons_eq_single_succ_iff {n : ℕ} (i : Fin n) {M : Type u_1} [Zero M] {y : M} {s : Fin n →₀ M} {x : M} : cons x s = single i.succ y ↔ s = single i y ∧ x = 0