Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-10 10:51 702b1e8c

View on Github →

refactor(data/finsupp/basic): merge finsupp.of_multiset and multiset.to_finsupp (#5237)

redefine finsupp.to_multiset as an add_equiv;
drop finsupp.equiv_multiset and finsupp.of_multiset;
define multiset.to_finsupp as finsupp.to_multiset.symm.

Estimated changes

Modified src/algebra/big_operators/basic.lean

modified theorem multiset.to_finset_sum_count_smul_eq

Modified src/data/finsupp/basic.lean

added theorem finsupp.coe_order_iso_multiset

added theorem finsupp.coe_order_iso_multiset_symm

deleted def finsupp.equiv_multiset

added theorem finsupp.le_def

modified theorem finsupp.mem_antidiagonal_support

deleted def finsupp.of_multiset

deleted theorem finsupp.of_multiset_apply

added def finsupp.order_iso_multiset

modified theorem finsupp.prod_to_multiset

modified theorem finsupp.to_finset_to_multiset

modified def finsupp.to_multiset

added theorem finsupp.to_multiset_apply

modified theorem finsupp.to_multiset_single

modified theorem finsupp.to_multiset_to_finsupp

modified def multiset.to_finsupp

modified theorem multiset.to_finsupp_add

added theorem multiset.to_finsupp_eq_iff

modified theorem multiset.to_finsupp_singleton

modified theorem multiset.to_finsupp_zero

added theorem multiset.to_finsuppstrict_mono

Modified src/data/finsupp/lattice.lean

deleted theorem finsupp.le_def

deleted theorem finsupp.of_multiset_strict_mono

deleted def finsupp.order_iso_multiset

deleted theorem finsupp.order_iso_multiset_apply

deleted theorem finsupp.order_iso_multiset_symm_apply

Modified src/logic/function/basic.lean

added theorem function.id_def