Theorem List.sum_map_le_apply_prod

Modification history

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