# Commit 2024-07-08 16:16 b9a098b6

View on Github →feat: add lemma `List.prod_map_ite_eq`

(#13023)
Proves that the (product) sum of a list mapped through a function of the form `if x = a then ... else ...`

is equal to the (product) sum over the list mapped through the else condition, (times) plus an additional factor about the number of times `a`

appears.
Upstreamed from another project.