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 α) : ∑ x ∈ Finset.insertNone s, f x = f none + ∑ x ∈ s, f (some x)

@[simp]

theorem Finset.prod_insertNone {α : Type u_1} {M : Type u_2} [CommMonoid M] (f : Option α → M) (s : Finset α) : ∏ x ∈ Finset.insertNone s, f x = f none * ∏ x ∈ s, 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 + ∑ i ∈ s, f i = ∑ i ∈ Finset.insertNone s, 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 * ∏ i ∈ s, f i = ∏ i ∈ Finset.insertNone s, i.elim x f

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

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