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' (M : Type u_1) [Zero M] : (Fin 2 →₀ M) ≃ M × M

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

Equations

• finTwoArrowEquiv' M = Finsupp.equivFunOnFinite.trans (finTwoArrowEquiv M)

@[simp]

theorem finTwoArrowEquiv'_symm_apply (M : Type u_1) [Zero M] (a✝ : M × M) : (finTwoArrowEquiv' M).symm a✝ = Finsupp.equivFunOnFinite.symm ![a✝.1, a✝.2]

@[simp]

theorem finTwoArrowEquiv'_apply (M : Type u_1) [Zero M] (a✝ : Fin 2 →₀ M) : (finTwoArrowEquiv' M) a✝ = (a✝ 0, a✝ 1)

theorem finTwoArrowEquiv'_sum_eq {M : Type u_1} {d : M × M} [AddCommMonoid M] : (((finTwoArrowEquiv' M).symm d).sum fun (x : Fin 2) (n : M) => n) = d.1 + d.2