Commit 2023-11-27 10:05 3f5910bf
View on Github →feat(Data/Finset/Card): add converse to some existing theorems (#8515)
- Add
Multiset.toFinset_card_eq_card_iff_nodup
which is converse toMultiset.toFinset_card_of_nodup
(credits: @Ruben-VandeVelde) - Add
Finset.card_eq_of_equiv_fin
andFinset.card_eq_of_equiv
which are converse toFinset.equivFinOfCardEq
andFinset.equivOfCardEq
, respectively. I'm not sure for the necessarily of these two, since they are also easy corollaries ofFintype.card_eq
andFintype.card_coe
.