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.

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

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

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