Lemmas about products and sums over finite sets in Option α

In this file we prove formulas for products and sums over Finset.insertNone s and Finset.eraseNone s.

@[simp]

theorem Finset.sum_insertNone {α : Type u_1} {M : Type u_2} [AddCommMonoid M] (f : Option α → M) (s : Finset α) : (Finset.sum (Finset.insertNone s) fun (x : Option α) => f x) = f none + Finset.sum s fun (x : α) => f (some x)

@[simp]

theorem Finset.prod_insertNone {α : Type u_1} {M : Type u_2} [CommMonoid M] (f : Option α → M) (s : Finset α) : (Finset.prod (Finset.insertNone s) fun (x : Option α) => f x) = f none * Finset.prod s fun (x : α) => f (some x)

theorem Finset.add_sum_eq_sum_insertNone {α : Type u_1} {M : Type u_2} [AddCommMonoid M] (f : α → M) (x : M) (s : Finset α) : (x + Finset.sum s fun (i : α) => f i) = Finset.sum (Finset.insertNone s) fun (i : Option α) => Option.elim i x f

theorem Finset.mul_prod_eq_prod_insertNone {α : Type u_1} {M : Type u_2} [CommMonoid M] (f : α → M) (x : M) (s : Finset α) : (x * Finset.prod s fun (i : α) => f i) = Finset.prod (Finset.insertNone s) fun (i : Option α) => Option.elim i x f

theorem Finset.sum_eraseNone {α : Type u_1} {M : Type u_2} [AddCommMonoid M] (f : α → M) (s : Finset (Option α)) : (Finset.sum (Finset.eraseNone s) fun (x : α) => f x) = Finset.sum s fun (x : Option α) => Option.elim' 0 f x

theorem Finset.prod_eraseNone {α : Type u_1} {M : Type u_2} [CommMonoid M] (f : α → M) (s : Finset (Option α)) : (Finset.prod (Finset.eraseNone s) fun (x : α) => f x) = Finset.prod s fun (x : Option α) => Option.elim' 1 f x