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.