Commit 2021-04-16 05:10 bb9b850e

View on Github →

feat(data/multiset/basic): some multiset lemmas, featuring sum inequalities (#7090) Proves some lemmas about rel and about inequalities between sums of multisets.

Estimated changes

Modified src/data/multiset/basic.lean

added theorem multiset.card_nsmul_le_sum

modified theorem multiset.map_nsmul

added theorem multiset.rel_of_forall

added theorem multiset.rel_refl_of_refl_on

added theorem multiset.rel_repeat_left

added theorem multiset.rel_repeat_right

added theorem multiset.sum_le_card_nsmul

added theorem multiset.sum_le_sum_map

added theorem multiset.sum_le_sum_of_rel_le

added theorem multiset.sum_map_le_sum