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} [inst : AddCommMonoid M] (f : Option αM) (s : Finset α) :
(Finset.sum (Finset.insertNone.toEmbedding 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} [inst : CommMonoid M] (f : Option αM) (s : Finset α) :
(Finset.prod (Finset.insertNone.toEmbedding s) fun x => f x) = f none * Finset.prod s fun x => f (some x)
theorem Finset.sum_eraseNone {α : Type u_1} {M : Type u_2} [inst : 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} [inst : 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