Commit 2023-02-06 08:37 b54b1497

View on Github →

feat: port Data.Multiset.Fintype (#1828)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Multiset/Fintype.lean

added def Multiset.ToType

added theorem Multiset.card_coe

added theorem Multiset.card_toEnumFinset

added def Multiset.coeEmbedding

added def Multiset.coeEquiv

added theorem Multiset.coe_eq

added theorem Multiset.coe_mem

added theorem Multiset.coe_mk

added theorem Multiset.image_toEnumFinset_fst

added theorem Multiset.map_toEnumFinset_fst

added theorem Multiset.map_univ

added theorem Multiset.map_univ_coe

added theorem Multiset.map_univ_coeEmbedding

added theorem Multiset.mem_of_mem_toEnumFinset

added theorem Multiset.mem_toEnumFinset

added def Multiset.mkToType

added theorem Multiset.prod_eq_prod_coe

added theorem Multiset.prod_eq_prod_toEnumFinset

added theorem Multiset.prod_toEnumFinset

added theorem Multiset.toEmbedding_coeEquiv_trans

added def Multiset.toEnumFinset

added theorem Multiset.toEnumFinset_filter_eq

added theorem Multiset.toEnumFinset_mono

added theorem Multiset.toEnumFinset_subset_iff