Commit 2025-11-05 21:27 29d85a07

View on Github →

feat: {List,Multiset,Finset}.prod_le_sum (#31012)

Estimated changes

Modified Mathlib/Algebra/MvPolynomial/Degrees.lean

modified theorem MvPolynomial.totalDegree_list_prod

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

added theorem Finset.apply_prod_le_sum_apply

added theorem Finset.sum_apply_le_apply_prod

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

added theorem List.apply_prod_le_sum_map

added theorem List.sum_map_le_apply_prod

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

added theorem Multiset.apply_prod_le_sum_map

added theorem Multiset.sum_map_le_apply_prod

Modified Mathlib/Algebra/Polynomial/BigOperators.lean

modified theorem Polynomial.degree_list_prod_le

modified theorem Polynomial.natDegree_list_prod_le

Modified Mathlib/Analysis/Normed/Group/Basic.lean

modified theorem enorm_prod_le

modified theorem norm_multiset_prod_le

modified theorem norm_prod_le