Theorem Finset.one_lt_prod_iff

Modification history

2025-07-18 11:35
Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
feat: Finset.sum_pos_iff (#27161)
Added Finset.one_lt_prod_iffView on Github →