Theorem Finset.sum_apply_le_apply_prod

Modification history

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