Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-24 15:33 68acd760

View on Github →

feat(group_theory/perm): perm.fintype and card_perm (closed #366)

Estimated changes

added theorem card_perms_of_finset
added theorem fintype.card_equiv
added theorem fintype.card_perm
added def fintype_perm
added theorem length_perms_of_list
added theorem mem_perms_of_list_iff
added theorem nodup_perms_of_list
added def perms_of_finset
added def perms_of_list