A product of factors that are u or 1

A candidate for Mathlib.Algebra.BigOperators.Group.List.Basic, next to List.prod_map_ite: the product over a list of u for the entries that pass a test and 1 for the others is u to the number of the entries that pass, in any monoid.

Main statements

• List.prod_map_ite_eq_pow: the product of u or 1 over a list is a power of u.

theorem List.prod_map_ite_eq_pow {α : Type u_1} {M : Type u_2} [Monoid M] (p : α → Bool) (u : M) (l : List α) : (map (fun (x : α) => if p x = true then u else 1) l).prod = u ^ (filter p l).length

theorem List.sum_map_ite_eq_nsmul {α : Type u_1} {M : Type u_2} [AddMonoid M] (p : α → Bool) (u : M) (l : List α) : (map (fun (x : α) => if p x = true then u else 0) l).sum = (filter p l).length • u