mathlib3 documentation

data.finsupp.fin

cons and tail for maps fin n →₀ M #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

noncomputable def finsupp.tail {n : } {M : Type u_1} [has_zero M] (s : fin (n + 1) →₀ M) :

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

Equations
noncomputable def finsupp.cons {n : } {M : Type u_1} [has_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
theorem finsupp.tail_apply {n : } (i : fin n) {M : Type u_1} [has_zero M] (t : fin (n + 1) →₀ M) :
(t.tail) i = t i.succ
@[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.cons_succ {n : } (i : fin n) {M : Type u_1} [has_zero M] (y : M) (s : fin n →₀ M) :
@[simp]
theorem finsupp.tail_cons {n : } {M : Type u_1} [has_zero M] (y : M) (s : fin n →₀ M) :
@[simp]
theorem finsupp.cons_tail {n : } {M : Type u_1} [has_zero M] (t : fin (n + 1) →₀ M) :
@[simp]
theorem finsupp.cons_zero_zero {n : } {M : Type u_1} [has_zero M] :
theorem finsupp.cons_ne_zero_of_left {n : } {M : Type u_1} [has_zero M] {y : M} {s : fin n →₀ M} (h : y 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) :
theorem finsupp.cons_ne_zero_iff {n : } {M : Type u_1} [has_zero M] {y : M} {s : fin n →₀ M} :
finsupp.cons y s 0 y 0 s 0