Documentation

Mathlib.Algebra.BigOperators.Option

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