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} [] (f : M) (s : ) :
xFinset.insertNone s, f x = f none + xs, f (some x)
@[simp]
theorem Finset.prod_insertNone {α : Type u_1} {M : Type u_2} [] (f : M) (s : ) :
xFinset.insertNone s, f x = f none * xs, f (some x)
theorem Finset.add_sum_eq_sum_insertNone {α : Type u_1} {M : Type u_2} [] (f : αM) (x : M) (s : ) :
x + is, f i = iFinset.insertNone s, i.elim x f
theorem Finset.mul_prod_eq_prod_insertNone {α : Type u_1} {M : Type u_2} [] (f : αM) (x : M) (s : ) :
x * is, f i = iFinset.insertNone s, i.elim x f
theorem Finset.sum_eraseNone {α : Type u_1} {M : Type u_2} [] (f : αM) (s : Finset (Option α)) :
xFinset.eraseNone s, f x = xs, Option.elim' 0 f x
theorem Finset.prod_eraseNone {α : Type u_1} {M : Type u_2} [] (f : αM) (s : Finset (Option α)) :
xFinset.eraseNone s, f x = xs, Option.elim' 1 f x