Commit 2026-02-21 12:00 307fa255

View on Github →

chore: weaken PartialOrder to Preorder in IsOrderedMonoid hypothesis (#34295) This PR attempts to remove PartialOrder assumption in IsOrderedMonoid. The main objective is to make Finsupp.sum_le_sum available for preorder.

Estimated changes

modified theorem one_le_finprod'
modified theorem single_le_finprod
modified theorem Finset.apply_union_le_sum
modified theorem Finset.one_lt_prod'
modified theorem Finset.one_lt_prod
modified theorem Finset.one_lt_prod_iff
modified theorem Finset.prod_lt_one'
modified theorem Finset.prod_lt_one
modified theorem Finset.prod_lt_prod'
modified theorem Finset.single_lt_prod'
modified theorem List.one_lt_prod_of_one_lt
modified theorem List.single_le_prod
modified theorem Multiset.le_prod_of_mem
modified theorem Multiset.prod_eq_one_iff
modified theorem IsLowerSet.div_left
modified theorem IsLowerSet.inv
modified theorem IsUpperSet.div_left
modified theorem IsUpperSet.inv
modified theorem Filter.inv_atTop
modified theorem hasProd_one_iff_of_one_le