Commit 2025-10-09 08:14 60117332

View on Github →

chore(Algebra/Order/BigOperators/Group/{Finset, Multiset}): generalize results to (Mul)(Add)LeftMono (#29864) Generalize some stuff from IsOrdered(Add)Monoid to (Mul)(Add)LeftMono.

Estimated changes

Modified Mathlib/Algebra/Order/BigOperators/Group/Finset.lean

modified theorem Finset.abs_sum_of_nonneg'

modified theorem Finset.abs_sum_of_nonneg

modified theorem Finset.apply_union_le_sum

modified theorem Finset.exists_lt_of_prod_lt'

modified theorem Finset.le_prod_nonempty_of_submultiplicative

modified theorem Finset.le_prod_nonempty_of_submultiplicative_on_pred

modified theorem Finset.le_prod_of_submultiplicative

modified theorem Finset.le_prod_of_submultiplicative_on_pred

modified theorem Finset.mul_le_prod

modified theorem Finset.one_le_prod''

modified theorem Finset.one_le_prod'

modified theorem Finset.one_lt_prod_iff_of_one_le

modified theorem Finset.pow_card_le_prod

modified theorem Finset.prod_eq_one_iff_of_le_one'

modified theorem Finset.prod_eq_one_iff_of_one_le'

modified theorem Finset.prod_fiberwise_le_prod_of_one_le_prod_fiber'

modified theorem Finset.prod_image_le_of_one_le

modified theorem Finset.prod_le_one'

modified theorem Finset.prod_le_pow_card

modified theorem Finset.prod_le_prod'

modified theorem Finset.prod_le_prod_fiberwise_of_prod_fiber_le_one'

modified theorem Finset.prod_le_prod_of_subset_of_one_le'

modified theorem Finset.prod_le_univ_prod_of_one_le'

modified theorem Finset.prod_lt_one_iff_of_le_one

modified theorem Finset.prod_mono_set_of_one_le'

modified theorem Finset.single_le_prod'

Modified Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean

modified theorem Multiset.all_one_of_le_one_le_of_prod_eq_one

modified theorem Multiset.one_le_prod_of_one_le

modified theorem Multiset.pow_card_le_prod

modified theorem Multiset.prod_le_pow_card

modified theorem Multiset.prod_le_prod_map

modified theorem Multiset.prod_le_prod_of_rel_le

modified theorem Multiset.prod_map_le_prod

modified theorem Multiset.prod_map_le_prod_map

modified theorem Multiset.single_le_prod

Modified Mathlib/Algebra/Order/Group/Int/Sum.lean

Modified Mathlib/Data/NNRat/BigOperators.lean

Modified Mathlib/Tactic/Positivity/Finset.lean