Commit 2024-08-15 11:25 75cc36e8

View on Github →

chore: Golf prod_involution (#15832) ... and extract prod_ite_zero from the proof of prod_boole

Estimated changes

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

modified theorem Finset.prod_involution

added theorem Finset.prod_ninvolution

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

added theorem Finset.prod_ite_zero

added theorem Fintype.prod_ite_zero