Commit 2024-06-16 19:40 acdc9041

View on Github →

chore: Golf Finset.prod_ite_of_true (#13726) ... and friends. Also rename prod_of_empty to prod_of_isEmpty.

Estimated changes

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

modified theorem Finset.prod_dite_of_false

modified theorem Finset.prod_dite_of_true

modified theorem Finset.prod_ite_of_false

modified theorem Finset.prod_ite_of_true

deleted theorem Finset.prod_of_empty

added theorem Finset.prod_of_isEmpty

Modified Mathlib/Algebra/DirectSum/Internal.lean

Modified Mathlib/Analysis/Convex/Combination.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

deleted theorem MeasureTheory.Measure.sum_of_empty

added theorem MeasureTheory.Measure.sum_of_isEmpty