Commit 2024-10-07 17:59 ae8a2a18

View on Github →

feat(Algebra/Order/BigOperators/Group/*): max_prod_le, prod_min_le (#17496) List, Multiset, Finset : max_prod_le, max_sum_le, prod_min_le, prod_sum_le

Estimated changes

added theorem Finset.max_prod_le
added theorem Finset.prod_min_le
added theorem List.max_prod_le
added theorem List.prod_min_le
added theorem Multiset.max_prod_le
added theorem Multiset.prod_min_le