Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-19 04:48 056a7a1a

View on Github →

feat(data/multiset/interval): locally finite order on multisets (#17028)

Estimated changes

Created src/data/dfinsupp/multiset.lean

added def dfinsupp.to_multiset

added theorem dfinsupp.to_multiset_single

added theorem dfinsupp.to_multiset_to_dfinsupp

added def multiset.equiv_dfinsupp

added def multiset.to_dfinsupp

added theorem multiset.to_dfinsupp_apply

added theorem multiset.to_dfinsupp_le_to_dfinsupp

added theorem multiset.to_dfinsupp_repeat

added theorem multiset.to_dfinsupp_singleton

added theorem multiset.to_dfinsupp_support

added theorem multiset.to_dfinsupp_to_multiset

Modified src/data/multiset/basic.lean

added theorem multiset.add_hom_ext

added theorem multiset.repeat_add

added def multiset.repeat_add_monoid_hom

Created src/data/multiset/interval.lean

added theorem multiset.Icc_eq

added theorem multiset.card_Icc

added theorem multiset.card_Ico

added theorem multiset.card_Iic

added theorem multiset.card_Ioc

added theorem multiset.card_Ioo

Modified src/data/multiset/locally_finite.lean