Tuple operations on maps Fin n →₀ M

We interpret maps Fin n →₀ M as n-tuples of elements of M, and define the following operations:

• Finsupp.tail : the tail of a map Fin (n + 1) →₀ M, i.e., its last n entries;
• Finsupp.init : the initial of a map Fin n →₀ M, i.e., its first n - 1 entries;
• Finsupp.removeNth : removing an element at a given entry of a map Fin (n + 1) →₀ M;
• Finsupp.cons : adding an element at the beginning of an n-tuple, to get an n + 1-tuple;
• Finsupp.snoc : adding an element at the end of an n-tuple, to get an n + 1-tuple;
• Finsupp.insertNth : adding an element at a given entry of an n-tuple, to get an n + 1-tuple.

In this context, we prove some usual properties of these operations, analogous to those of Data.Fin.Tuple.Basic.

@[simp]

theorem Fin.prod_insertNth {β : Type u_2} [CommMonoid β] {n : ℕ} (x : β) (f : Fin n → β) (p : Fin (n + 1)) : ∏ i : Fin (n + 1), p.insertNth x f i = x * ∏ i : Fin n, f i

@[simp]

theorem Fin.sum_insertNth {β : Type u_2} [AddCommMonoid β] {n : ℕ} (x : β) (f : Fin n → β) (p : Fin (n + 1)) : ∑ i : Fin (n + 1), p.insertNth x f i = x + ∑ i : Fin n, f i

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

init for maps Fin n →₀ M. See Fin.init for more details.

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

removeNth for maps Fin n →₀ M. See Fin.removeNth for more details.

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

snoc for maps Fin n →₀ M. See Fin.snoc for more details.

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

insertNth for maps Fin n →₀ M. See Fin.insertNth for more details.

@[simp]

theorem Finsupp.removeNth_apply {n : ℕ} {M : Type u_1} [Zero M] (p : Fin (n + 1)) (s : Fin (n + 1) →₀ M) (i : Fin n) : (removeNth p s) i = s (p.succAbove i)

@[simp]

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

@[simp]

theorem Finsupp.removeNth_last {n : ℕ} {M : Type u_1} [Zero M] (s : Fin (n + 1) →₀ M) : removeNth (Fin.last n) s = s.init

@[simp]

theorem Finsupp.removeNth_update {n : ℕ} {M : Type u_1} [Zero M] (p : Fin (n + 1)) (s : Fin (n + 1) →₀ M) (y : M) : removeNth p (s.update p y) = removeNth p s

Updating the i-th entry does not affect removing the i-th entry.

@[simp]

theorem Finsupp.init_apply {n : ℕ} {M : Type u_1} [Zero M] (s : Fin (n + 1) →₀ M) (i : Fin n) : s.init i = s i.castSucc

@[simp]

theorem Finsupp.init_update_last {n : ℕ} {M : Type u_1} [Zero M] (s : Fin (n + 1) →₀ M) (y : M) : (s.update (Fin.last n) y).init = s.init

@[simp]

theorem Finsupp.init_update_castSucc {n : ℕ} {M : Type u_1} [Zero M] (s : Fin (n + 1) →₀ M) (y : M) (i : Fin n) : (s.update i.castSucc y).init = s.init.update i y

theorem Finsupp.tail_init_eq_init_tail {n : ℕ} {M : Type u_1} [Zero M] (s : Fin (n + 2) →₀ M) : s.init.tail = s.tail.init

@[simp]

theorem Finsupp.snoc_last {n : ℕ} {M : Type u_1} [Zero M] (y : M) (s : Fin n →₀ M) : (s.snoc y) (Fin.last n) = y

@[simp]

theorem Finsupp.snoc_castSucc {n : ℕ} {M : Type u_1} [Zero M] (y : M) (s : Fin n →₀ M) (i : Fin n) : (s.snoc y) i.castSucc = s i

@[simp]

theorem Finsupp.insertNth_zero {n : ℕ} {M : Type u_1} [Zero M] (y : M) (s : Fin n →₀ M) : insertNth 0 y s = cons y s

@[simp]

theorem Finsupp.insertNth_last {n : ℕ} {M : Type u_1} [Zero M] (y : M) (s : Fin n →₀ M) : insertNth (Fin.last n) y s = s.snoc y

@[simp]

theorem Finsupp.insertNth_apply_same {n : ℕ} {M : Type u_1} [Zero M] (p : Fin (n + 1)) (y : M) (s : Fin n →₀ M) : (insertNth p y s) p = y

@[simp]

theorem Finsupp.insertNth_apply_succAbove {n : ℕ} {M : Type u_1} [Zero M] (p : Fin (n + 1)) (y : M) (s : Fin n →₀ M) (i : Fin n) : (insertNth p y s) (p.succAbove i) = s i

@[simp]

theorem Finsupp.init_snoc {n : ℕ} {M : Type u_1} [Zero M] (y : M) (s : Fin n →₀ M) : (s.snoc y).init = s

@[simp]

theorem Finsupp.snoc_init_self {n : ℕ} {M : Type u_1} [Zero M] (t : Fin (n + 1) →₀ M) : t.init.snoc (t (Fin.last n)) = t

@[simp]

theorem Finsupp.insertNth_removeNth {n : ℕ} {M : Type u_1} [Zero M] (p : Fin (n + 1)) (y : M) (t : Fin (n + 1) →₀ M) : insertNth p y (removeNth p t) = t.update p y

theorem Finsupp.insertNth_self_removeNth {n : ℕ} {M : Type u_1} [Zero M] (p : Fin (n + 1)) (t : Fin (n + 1) →₀ M) : insertNth p (t p) (removeNth p t) = t

@[simp]

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

@[simp]

theorem Finsupp.insertNth_zero_zero {n : ℕ} {M : Type u_1} [Zero M] (p : Fin (n + 1)) : insertNth p 0 0 = 0

theorem Finsupp.snoc_ne_zero_of_left {n : ℕ} {M : Type u_1} [Zero M] {y : M} {s : Fin n →₀ M} (h : s ≠ 0) : s.snoc y ≠ 0

theorem Finsupp.snoc_ne_zero_of_right {n : ℕ} {M : Type u_1} [Zero M] {y : M} {s : Fin n →₀ M} (h : y ≠ 0) : s.snoc y ≠ 0

theorem Finsupp.snoc_ne_zero_iff {n : ℕ} {M : Type u_1} [Zero M] {y : M} {s : Fin n →₀ M} : s.snoc y ≠ 0 ↔ s ≠ 0 ∨ y ≠ 0

theorem Finsupp.insertNth_ne_zero_of_left {n : ℕ} {M : Type u_1} [Zero M] (p : Fin (n + 1)) {y : M} {s : Fin n →₀ M} (h : y ≠ 0) : insertNth p y s ≠ 0

theorem Finsupp.insertNth_ne_zero_of_right {n : ℕ} {M : Type u_1} [Zero M] (p : Fin (n + 1)) {y : M} {s : Fin n →₀ M} (h : s ≠ 0) : insertNth p y s ≠ 0

theorem Finsupp.insertNth_ne_zero_iff {n : ℕ} {M : Type u_1} [Zero M] (p : Fin (n + 1)) {y : M} {s : Fin n →₀ M} : insertNth p y s ≠ 0 ↔ y ≠ 0 ∨ s ≠ 0

theorem Finsupp.snoc_support {n : ℕ} {M : Type u_1} [Zero M] {y : M} {s : Fin n →₀ M} : (s.snoc y).support ⊆ insert (Fin.last n) (Finset.map Fin.castSuccEmb s.support)

theorem Finsupp.snoc_left_injective {n : ℕ} {M : Type u_1} [Zero M] {y : M} : Function.Injective fun (x : Fin n →₀ M) => x.snoc y

theorem Finsupp.insertNth_support {n : ℕ} {M : Type u_1} [Zero M] (p : Fin (n + 1)) {y : M} {s : Fin n →₀ M} : (insertNth p y s).support ⊆ insert p (Finset.map p.succAboveEmb s.support)

theorem Finsupp.insertNth_right_injective {n : ℕ} {M : Type u_1} [Zero M] (p : Fin (n + 1)) {y : M} : Function.Injective (insertNth p y)

theorem Finsupp.sum_insertNth {M : Type u_2} [AddCommMonoid M] {n : ℕ} (σ : Fin n →₀ M) (i : M) (p : Fin (n + 1)) : ((insertNth p i σ).sum fun (x : Fin (n + 1)) (e : M) => e) = i + σ.sum fun (x : Fin n) (e : M) => e

theorem Finsupp.sum_insertNth' {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] {n : ℕ} (σ : Fin n →₀ M) (i : M) (p : Fin (n + 1)) (f : Fin (n + 1) → M → N) (h : ∀ (x : Fin (n + 1)), f x 0 = 0) : (insertNth p i σ).sum f = f p i + σ.sum (p.removeNth f)