Commit 2023-02-19 00:43 59927331

View on Github →

feat: port Data.Dfinsupp.Multiset (#2345)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/DirectSum/Basic.lean

Modified Mathlib/Data/Dfinsupp/Basic.lean

added theorem Dfinsupp.addHom_ext'

added theorem Dfinsupp.addHom_ext

deleted theorem Dfinsupp.add_hom_ext'

deleted theorem Dfinsupp.add_hom_ext

Created Mathlib/Data/Dfinsupp/Multiset.lean

added def Dfinsupp.toMultiset

added theorem Dfinsupp.toMultiset_single

added theorem Dfinsupp.toMultiset_toDfinsupp

added def Multiset.equivDfinsupp

added def Multiset.toDfinsupp

added theorem Multiset.toDfinsupp_apply

added theorem Multiset.toDfinsupp_le_toDfinsupp

added theorem Multiset.toDfinsupp_replicate

added theorem Multiset.toDfinsupp_singleton

added theorem Multiset.toDfinsupp_support

added theorem Multiset.toDfinsupp_toMultiset