Absolute values and sums/products over multisets #
This file contains lemmas on the relation between Multiset.prod/Multiset.sum and abs.
Main declarations #
Multiset.abs_sum_le_sum_abs: the multiset version of the triangle inequality.
theorem
Multiset.abs_sum_le_sum_abs
{α : Type u_1}
[LinearOrderedAddCommGroup α]
{s : Multiset α}
:
|Multiset.sum s| ≤ Multiset.sum (Multiset.map abs s)