Commit 2023-02-05 17:34 801069df

View on Github →

feat: Port Data.Fintype.Perm (#1691) Port of data.fintype.perm

Estimated changes

added theorem Fintype.card_equiv
added theorem Fintype.card_perm
added theorem card_perms_of_finset
added def fintypePerm
added theorem length_permsOfList
added theorem mem_of_mem_permsOfList
added theorem mem_permsOfList_iff
added theorem mem_permsOfList_of_mem
added theorem nodup_permsOfList
added def permsOfFinset
added def permsOfList