Commit 2024-09-22 18:19 ed1a8a03

View on Github →

feat: Fintype.prod_ite_mem (#17017) This specializes the existing Finset.prod_ite_mem. From LeanAPAP

Estimated changes

Modified Mathlib/Algebra/BigOperators/Group/Finset.lean

added theorem Fintype.prod_ite_mem

Modified Mathlib/Algebra/Module/BigOperators.lean

Modified Mathlib/Combinatorics/SetFamily/FourFunctions.lean