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 α) :
@[simp]
theorem
finset.sum_insert_none
{α : Type u_1}
{M : Type u_2}
[add_comm_monoid M]
(f : option α → M)
(s : finset α) :
theorem
finset.prod_erase_none
{α : Type u_1}
{M : Type u_2}
[comm_monoid M]
(f : α → M)
(s : finset (option α)) :
∏ (x : α) in ⇑finset.erase_none s, f x = ∏ (x : option α) in s, 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 α)) :
∑ (x : α) in ⇑finset.erase_none s, f x = ∑ (x : option α) in s, x.elim 0 f