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.insertNone s).sum fun (x : Option α) => f x) = f none + s.sum 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.insertNone s).prod fun (x : Option α) => f x) = f none * s.prod 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 + s.sum fun (i : α) => f i) = (Finset.insertNone s).sum fun (i : Option α) => i.elim 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 * s.prod fun (i : α) => f i) = (Finset.insertNone s).prod fun (i : Option α) => i.elim x f

theorem Finset.sum_eraseNone {α : Type u_1} {M : Type u_2} [AddCommMonoid M] (f : α → M) (s : Finset (Option α)) : ((Finset.eraseNone s).sum fun (x : α) => f x) = s.sum 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.eraseNone s).prod fun (x : α) => f x) = s.prod fun (x : Option α) => Option.elim' 1 f x