Theorem Multiset.sum_map_le_apply_prod

Modification history

2025-11-05 21:27
Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean
feat: {List,Multiset,Finset}.prod_le_sum (#31012)
Added Multiset.sum_map_le_apply_prodView on Github →