Commit 2025-01-22 09:20 ca7a3cdb

View on Github →

feat(Multiset/Fintype): Multiset.ToType equivalence between v ::ₘ m and Option m (#19508) Also add an arbitrary equivalence s ≃ s.map f

Estimated changes

Modified Mathlib/Data/Multiset/Fintype.lean

modified def Multiset.ToType

modified theorem Multiset.card_coe

modified theorem Multiset.card_toEnumFinset

added def Multiset.cast

modified def Multiset.coeEmbedding

modified def Multiset.coeEquiv

added theorem Multiset.coe_consEquiv_of_eq_of_eq

added theorem Multiset.coe_consEquiv_of_eq_of_lt

added theorem Multiset.coe_consEquiv_of_ne

modified theorem Multiset.coe_mem

modified theorem Multiset.coe_mk

added def Multiset.consEquiv

added theorem Multiset.consEquiv_symm_none

added theorem Multiset.consEquiv_symm_some

added theorem Multiset.mapEquiv_apply

added def Multiset.mapEquiv_aux

modified theorem Multiset.map_univ

modified theorem Multiset.map_univ_coe

modified theorem Multiset.map_univ_coeEmbedding

modified theorem Multiset.mem_of_mem_toEnumFinset

modified theorem Multiset.mem_toEnumFinset

modified def Multiset.mkToType

modified theorem Multiset.prod_eq_prod_coe

modified theorem Multiset.prod_eq_prod_toEnumFinset

modified theorem Multiset.prod_toEnumFinset

modified theorem Multiset.toEmbedding_coeEquiv_trans

modified def Multiset.toEnumFinset

modified theorem Multiset.toEnumFinset_mono

modified theorem Multiset.toEnumFinset_subset_iff