# Documentation

Mathlib.Data.Fintype.Perm

# Fintype instances for Equiv and Perm#

Main declarations:

• permsOfFinset s: The finset of permutations of the finset s.
def permsOfList {α : Type u_1} [] :
List αList ()

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

Equations
Instances For
theorem length_permsOfList {α : Type u_1} [] (l : List α) :
theorem mem_permsOfList_of_mem {α : Type u_1} [] {l : List α} {f : } (h : ∀ (x : α), f x xx l) :
f
theorem mem_of_mem_permsOfList {α : Type u_1} [] {l : List α} {f : } :
f ∀ (x : α), f x xx l
theorem mem_permsOfList_iff {α : Type u_1} [] {l : List α} {f : } :
f ∀ {x : α}, f x xx l
theorem nodup_permsOfList {α : Type u_1} [] {l : List α} :
def permsOfFinset {α : Type u_1} [] (s : ) :

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

Instances For
theorem mem_perms_of_finset_iff {α : Type u_1} [] {s : } {f : } :
∀ {x : α}, f x xx s
theorem card_perms_of_finset {α : Type u_1} [] (s : ) :
def fintypePerm {α : Type u_1} [] [] :

The collection of permutations of a fintype is a fintype.

Instances For
instance equivFintype {α : Type u_1} {β : Type u_2} [] [] [] [] :
Fintype (α β)
theorem Fintype.card_perm {α : Type u_1} [] [] :
theorem Fintype.card_equiv {α : Type u_1} {β : Type u_2} [] [] [] [] (e : α β) :
Fintype.card (α β) =