Finsupp.sum and Finsupp.prod over Fin

This file contains theorems relevant to big operators in 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} [AddCommMonoid 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)