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.

Estimated changes