Commit 2021-11-15 21:01 9c03e9dc
View on Github →feat(data/fintype): computable trunc bijection from fin (#10141)
When a type X lacks decidable equality, there is still computably a bijection fin (card X) -> X using trunc.
Also, move fintype.equiv_fin_of_forall_mem_list to list.nodup.nth_le_equiv_of_forall_mem_list.