Theorem Finset.one_lt_prod_iff_of_one_le

Modification history

2026-02-21 12:00
Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
chore: weaken `PartialOrder` to `Preorder` in `IsOrderedMonoid` hypothesis (#34295) …
Modified Finset.one_lt_prod_iff_of_one_leView on Github →
2025-10-09 08:14
Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
chore(Algebra/Order/BigOperators/Group/{Finset, Multiset}): generalize results to `(Mul)(Add)LeftMono` (#29864) …
Modified Finset.one_lt_prod_iff_of_one_leView on Github →
2025-07-18 11:35
Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
feat: Finset.sum_pos_iff (#27161)
Added Finset.one_lt_prod_iff_of_one_leView on Github →