Commit 2021-12-29 21:58 5ac87153

View on Github →

split(data/finsupp/multiset): Split off data.finsupp.basic (#11110) This moves finsupp.to_multiset, multiset.to_finsupp and finsupp.order_iso_multiset to a new file data.finsupp.multiset.

Estimated changes

Modified src/data/finsupp/antidiagonal.lean

Modified src/data/finsupp/basic.lean

deleted theorem finsupp.card_to_multiset

deleted theorem finsupp.count_to_multiset

deleted theorem finsupp.mem_to_multiset

deleted theorem finsupp.prod_to_multiset

deleted theorem finsupp.to_finset_to_multiset

deleted def finsupp.to_multiset

deleted theorem finsupp.to_multiset_add

deleted theorem finsupp.to_multiset_apply

deleted theorem finsupp.to_multiset_map

deleted theorem finsupp.to_multiset_single

deleted theorem finsupp.to_multiset_sum

deleted theorem finsupp.to_multiset_sum_single

deleted theorem finsupp.to_multiset_symm_apply

deleted theorem finsupp.to_multiset_to_finsupp

deleted theorem finsupp.to_multiset_zero

deleted def multiset.to_finsupp

deleted theorem multiset.to_finsupp_add

deleted theorem multiset.to_finsupp_apply

deleted theorem multiset.to_finsupp_eq_iff

deleted theorem multiset.to_finsupp_singleton

deleted theorem multiset.to_finsupp_support

deleted theorem multiset.to_finsupp_to_multiset

deleted theorem multiset.to_finsupp_zero

Created src/data/finsupp/multiset.lean

added theorem finsupp.card_to_multiset

added theorem finsupp.coe_order_iso_multiset

added theorem finsupp.coe_order_iso_multiset_symm

added theorem finsupp.count_to_multiset

added theorem finsupp.lt_wf

added theorem finsupp.mem_to_multiset

added def finsupp.order_iso_multiset

added theorem finsupp.prod_to_multiset

added theorem finsupp.sum_id_lt_of_lt

added theorem finsupp.to_finset_to_multiset

added def finsupp.to_multiset

added theorem finsupp.to_multiset_add

added theorem finsupp.to_multiset_apply

added theorem finsupp.to_multiset_map

added theorem finsupp.to_multiset_single

added theorem finsupp.to_multiset_strict_mono

added theorem finsupp.to_multiset_sum

added theorem finsupp.to_multiset_sum_single

added theorem finsupp.to_multiset_symm_apply

added theorem finsupp.to_multiset_to_finsupp

added theorem finsupp.to_multiset_zero

added def multiset.to_finsupp

added theorem multiset.to_finsupp_add

added theorem multiset.to_finsupp_apply

added theorem multiset.to_finsupp_eq_iff

added theorem multiset.to_finsupp_singleton

added theorem multiset.to_finsupp_strict_mono

added theorem multiset.to_finsupp_support

added theorem multiset.to_finsupp_to_multiset

added theorem multiset.to_finsupp_zero

Modified src/data/finsupp/order.lean

deleted theorem finsupp.coe_order_iso_multiset

deleted theorem finsupp.coe_order_iso_multiset_symm

deleted theorem finsupp.lt_wf

deleted def finsupp.order_iso_multiset

deleted theorem finsupp.sum_id_lt_of_lt

deleted theorem finsupp.to_multiset_strict_mono

deleted theorem multiset.to_finsupp_strict_mono

Modified src/ring_theory/unique_factorization_domain.lean