Commit 2024-12-18 01:49 d8e48a35

feat(BigOperators): prod_ite_eq_of_mem (#20026) I found these lemmas very helpful for manipulating sums in my Selberg sieve project. The benefit these lemmas have over prod_ite_eq and prod_ite_eq' is that the RHS is not an if-then-else block, which makes it much more useful for rewriting backwards to introduce a sum.