Commit 2021-05-03 21:31 67dad976

chore(data/fintype): rework fintype.equiv_fin and dependencies (#7136) These changes should make the declarations fintype.equiv_fin, fintype.card_eq and fintype.equiv_of_card_eq more convenient to use. Renamed:

• fintype.equiv_fin -> fintype.trunc_equiv_fin Deleted:
• fintype.nonempty_equiv_of_card_eq (use fintype.equiv_of_card_eq instead)
• fintype.exists_equiv_fin (use fintype.card and fintype.(trunc_)equiv_fin instead) Added:
• fintype.equiv_fin: noncomputable, non-trunc version of fintype.equiv_fin
• fintype.equiv_of_card_eq: noncomputable, non-trunc version of fintype.trunc_equiv_of_card_eq
• fintype.(trunc_)equiv_fin_of_card_eq (intermediate result/specialization of fintype.(trunc_)equiv_of_card_eq Zulip thread