Theorem Multiset.apply_prod_le_sum_map

Modification history

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