Commit 2023-02-03 18:59 88a42cbe

View on Github →

feat: port Data.Finsupp.Multiset (#1988) Some proofs needed rewriting because or different unfolding behaviour of Equivs and toFuns, but in the end it was not too bad. Revisiting Hom/Equiv/Basic might be valuable at some point

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finsupp/Multiset.lean

added theorem Finsupp.card_toMultiset

added theorem Finsupp.coe_orderIsoMultiset

added theorem Finsupp.coe_orderIsoMultiset_symm

added theorem Finsupp.count_toMultiset

added theorem Finsupp.lt_wf

added theorem Finsupp.mem_toMultiset

added def Finsupp.orderIsoMultiset

added theorem Finsupp.prod_toMultiset

added theorem Finsupp.sum_id_lt_of_lt

added theorem Finsupp.toFinset_toMultiset

added def Finsupp.toMultiset

added theorem Finsupp.toMultiset_add

added theorem Finsupp.toMultiset_apply

added theorem Finsupp.toMultiset_map

added theorem Finsupp.toMultiset_single

added theorem Finsupp.toMultiset_strictMono

added theorem Finsupp.toMultiset_sum

added theorem Finsupp.toMultiset_sum_single

added theorem Finsupp.toMultiset_symm_apply

added theorem Finsupp.toMultiset_toFinsupp

added theorem Finsupp.toMultiset_zero

added def Multiset.toFinsupp

added theorem Multiset.toFinsupp_add

added theorem Multiset.toFinsupp_apply

added theorem Multiset.toFinsupp_eq_iff

added theorem Multiset.toFinsupp_singleton

added theorem Multiset.toFinsupp_strictMono

added theorem Multiset.toFinsupp_support

added theorem Multiset.toFinsupp_toMultiset

added theorem Multiset.toFinsupp_zero