mathlib documentation

algebra.big_operators.option

Lemmas about products and sums over finite sets in option α #

In this file we prove formulas for products and sums over finset.insert_none s and finset.erase_none s.

@[simp]
theorem finset.prod_insert_none {α : Type u_1} {M : Type u_2} [comm_monoid M] (f : option α → M) (s : finset α) :
(finset.insert_none s).prod (λ (x : option α), f x) = f option.none * s.prod (λ (x : α), f (option.some x))
@[simp]
theorem finset.sum_insert_none {α : Type u_1} {M : Type u_2} [add_comm_monoid M] (f : option α → M) (s : finset α) :
(finset.insert_none s).sum (λ (x : option α), f x) = f option.none + s.sum (λ (x : α), f (option.some x))
theorem finset.prod_erase_none {α : Type u_1} {M : Type u_2} [comm_monoid M] (f : α → M) (s : finset (option α)) :
(finset.erase_none s).prod (λ (x : α), f x) = s.prod (λ (x : option α), x.elim 1 f)
theorem finset.sum_erase_none {α : Type u_1} {M : Type u_2} [add_comm_monoid M] (f : α → M) (s : finset (option α)) :
(finset.erase_none s).sum (λ (x : α), f x) = s.sum (λ (x : option α), x.elim 0 f)