Lemmas about products and sums over finite sets in option α #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 α), option.elim 1 f x)
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 α), option.elim 0 f x)