# mathlib3documentation

data.fintype.perm

# fintype instances for equiv and perm#

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main declarations:

• perms_of_finset s: The finset of permutations of the finset s.
def perms_of_list {α : Type u_1} [decidable_eq α] :

Given a list, produce a list of all permutations of its elements.

Equations
theorem length_perms_of_list {α : Type u_1} [decidable_eq α] (l : list α) :
theorem mem_perms_of_list_of_mem {α : Type u_1} [decidable_eq α] {l : list α} {f : equiv.perm α} (h : (x : α), f x x x l) :
theorem mem_of_mem_perms_of_list {α : Type u_1} [decidable_eq α] {l : list α} {f : equiv.perm α} :
{x : α}, f x x x l
theorem mem_perms_of_list_iff {α : Type u_1} [decidable_eq α] {l : list α} {f : equiv.perm α} :
{x : α}, f x x x l
theorem nodup_perms_of_list {α : Type u_1} [decidable_eq α] {l : list α} (hl : l.nodup) :
def perms_of_finset {α : Type u_1} [decidable_eq α] (s : finset α) :

Given a finset, produce the finset of all permutations of its elements.

Equations
theorem mem_perms_of_finset_iff {α : Type u_1} [decidable_eq α] {s : finset α} {f : equiv.perm α} :
{x : α}, f x x x s
theorem card_perms_of_finset {α : Type u_1} [decidable_eq α] (s : finset α) :
def fintype_perm {α : Type u_1} [decidable_eq α] [fintype α] :

The collection of permutations of a fintype is a fintype.

Equations
@[protected, instance]
def equiv.fintype {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] :
fintype β)
Equations
theorem fintype.card_perm {α : Type u_1} [decidable_eq α] [fintype α] :
theorem fintype.card_equiv {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] (e : α β) :
fintype.card β) =