Big operators over finite sets of optional values

This file splits a product or sum over Finset (Option α) into the terms indexed by some and the possible term indexed by none.

Main results

• Finset.prod_option: split a product into its some terms and its possible none term.
• Finset.sum_option: additive version of Finset.prod_option.

theorem Finset.prod_option {α : Type u_1} {M : Type u_2} [DecidableEq α] [CommMonoid M] (s : Finset (Option α)) (f : Option α → M) : ∏ x ∈ s, f x = (∏ x ∈ eraseNone s, f (some x)) * if none ∈ s then f none else 1

Split a product over optional values into its some terms and its possible none term.

theorem Finset.sum_option {α : Type u_1} {M : Type u_2} [DecidableEq α] [AddCommMonoid M] (s : Finset (Option α)) (f : Option α → M) : ∑ x ∈ s, f x = ∑ x ∈ eraseNone s, f (some x) + if none ∈ s then f none else 0

Split a sum over optional values into its some terms and its possible none term.