Products of indicators over a list

In a monoid with zero, the product over a list of the indicators if p a then 1 else 0 is the indicator that p holds at every element of the list (List.prod_map_boole). This is the list form of Finset.prod_boole.

Main results

• List.prod_map_boole: a product of indicators is the indicator of the conjunction.

theorem List.prod_map_boole {M₀ : Type u_1} {α : Type u_2} [MonoidWithZero M₀] (l : List α) (p : α → Prop) [DecidablePred p] : (map (fun (a : α) => if p a then 1 else 0) l).prod = if ∀ (a : α), a ∈ l → p a then 1 else 0

A product of indicators is the indicator of the conjunction.