Commit 2025-01-20 11:09 43e08d28

feat(BigOperators): ite_prod_one / ite_sum_zero (#20779) These lemmas were useful for manipulating nested sums while working on the Selberg sieve. They can be used to push a condition from the outer sum into an inner sum.