Theorem Finset.apply_prod_le_sum_apply

Modification history

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