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 to Multiset.toFinset_card_of_nodup (credits: @Ruben-VandeVelde)
  • Add Finset.card_eq_of_equiv_fin and Finset.card_eq_of_equiv which are converse to Finset.equivFinOfCardEq and Finset.equivOfCardEq, respectively. I'm not sure for the necessarily of these two, since they are also easy corollaries of Fintype.card_eq and Fintype.card_coe.

Estimated changes