Theorem Finset.prod_le_one
Modification history
2024-05-27 08:32
Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean
chore: Use the new `∑ i ∈ s, f i` notation (#13209) …
Modified Finset.prod_le_oneView on Github →2024-04-05 15:59
Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
chore: Sort big operator order lemmas (#11750) …
Modified Finset.prod_le_oneView on Github →