Documentation

Mathlib.Data.Finsupp.Fin

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:

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

def Finsupp.tail {n : } {M : Type u_1} [Zero M] (s : Fin (n + 1) →₀ 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
    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
    Instances For
      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) :
      (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
      @[simp]
      theorem Finsupp.cons_zero_zero {n : } {M : Type u_1} [Zero M] :
      theorem Finsupp.cons_ne_zero_of_left {n : } {M : Type u_1} [Zero M] {y : M} {s : Fin n →₀ M} (h : y 0) :
      theorem Finsupp.cons_ne_zero_of_right {n : } {M : Type u_1} [Zero M] {y : M} {s : Fin n →₀ M} (h : s 0) :
      theorem Finsupp.cons_ne_zero_iff {n : } {M : Type u_1} [Zero M] {y : M} {s : Fin n →₀ M} :
      Finsupp.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} :
      (Finsupp.cons y s).support insert 0 (Finset.map (Fin.succEmb n) s.support)