Commit 2025-04-30 16:43 bcc1a2a2

View on Github →

feat(Algebra/Order/BigOperator): add lemmas (#23266)

Estimated changes

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

added theorem Finset.le_prod_of_submultiplicative_of_nonneg

added theorem Finset.le_prod_of_submultiplicative_on_pred_of_nonneg

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

added theorem Multiset.le_prod_of_submultiplicative_of_nonneg

added theorem Multiset.le_prod_of_submultiplicative_on_pred_of_nonneg

Modified Mathlib/Data/Finset/Max.lean

added theorem Multiset.exists_max_image

added theorem Multiset.exists_min_image