Commit 2025-07-18 11:35 26133a63

View on Github →

feat: Finset.sum_pos_iff (#27161)

Estimated changes

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

added theorem Finset.one_lt_prod_iff

added theorem Finset.one_lt_prod_iff_of_one_le

added theorem Finset.prod_lt_one_iff_of_le_one