mathlib

bb9b850e - feat(data/multiset/basic): some multiset lemmas, featuring sum inequalities (#7090)

feat(data/multiset/basic): some multiset lemmas, featuring sum inequalities (#7090) Proves some lemmas about `rel` and about inequalities between sums of multisets. Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>