Finsupp.sum and Finsupp.prod over Fin

This file contains theorems relevant to big operators on finitely supported functions over Fin.

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

theorem Finsupp.sum_cons' {M : Type u_1} {N : Type u_2} [Zero M] [AddCommMonoid N] (n : ℕ) (σ : Fin n →₀ M) (i : M) (f : Fin (n + 1) → M → N) (h : ∀ (x : Fin (n + 1)), f x 0 = 0) : (cons i σ).sum f = f 0 i + σ.sum (Fin.tail f)

theorem Finsupp.ofSupportFinite_fin_two_eq (n : Fin 2 →₀ ℕ) : ofSupportFinite ![n 0, n 1] ⋯ = n

noncomputable def finTwoArrowEquiv' (X : Type u_1) [Zero X] : (Fin 2 →₀ X) ≃ X × X

The space of finitely supported functions Fin 2 →₀ α is equivalent to α × α. See also finTwoArrowEquiv.

Equations

• finTwoArrowEquiv' X = { toFun := fun (x : Fin 2 →₀ X) => (x 0, x 1), invFun := fun (x : X × X) => Finsupp.ofSupportFinite ![x.1, x.2] ⋯, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem finTwoArrowEquiv'_symm_apply (X : Type u_1) [Zero X] : ⇑(finTwoArrowEquiv' X).symm = fun (x : X × X) => Finsupp.ofSupportFinite ![x.1, x.2] ⋯

@[simp]

theorem finTwoArrowEquiv'_apply (X : Type u_1) [Zero X] : ⇑(finTwoArrowEquiv' X) = fun (x : Fin 2 →₀ X) => (x 0, x 1)

theorem finTwoArrowEquiv'_sum_eq {d : ℕ × ℕ} : (((finTwoArrowEquiv' ℕ).symm d).sum fun (x : Fin 2) (n : ℕ) => n) = d.1 + d.2