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 => 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 => 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.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.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.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.elim' 1 f x