English
Let l be a finite list with elements from a commutative monoid M, and p a predicate on the index α. For any function f : α → M, the product over the elements of l that satisfy p, together with the product over the elements that do not satisfy p, equals the product over all elements of l after applying f.
Русский
Пусть l — конечный список элементов в коммутативной моноиде M, и p — предикат на индексы α. Для любой функции f : α → M произведение по элементам списка l, удовлетворяющим p, умноженное на произведение по элементам, не удовлетворяющим p, равно произведению по всем элементам списка l после применения f.
LaTeX
$$$((l.filter p).map f).prod \cdot ((l.filter (fun x => \neg p x)).map f).prod = (l.map f).prod$$
Lean4
@[to_additive]
theorem prod_map_filter_mul_prod_map_filter_not (p : α → Prop) [DecidablePred p] (f : α → M) (l : List α) :
((l.filter p).map f).prod * ((l.filter fun x => ¬p x).map f).prod = (l.map f).prod :=
by
rw [← prod_map_ite]
simp only [ite_self]
