Commit 2024-12-05 16:41 36c7c9d4

View on Github →

feat(Algebra/BigOperators/Group/Finset) : Finset.prod_disjoint_filters (#19712) Decomposes the product(sum) over two filters where they are pointwise disjoint. Used in #19432

Estimated changes

added theorem Finset.prod_filter_xor