Theorem norm_multiset_prod_le

Modification history

2025-11-05 21:27
Mathlib/Analysis/Normed/Group/Basic.lean
feat: {List,Multiset,Finset}.prod_le_sum (#31012)
Modified norm_multiset_prod_leView on Github →
2023-03-09 06:58
Mathlib/Analysis/Normed/Group/Basic.lean
feat: port Analysis.Normed.Group.Basic (#2736)
Added norm_multiset_prod_leView on Github →