# Fintype instances for Equiv and Perm#

Main declarations:

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 α) :
().length = l.length.factorial
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 α} :
l.Nodup().Nodup
def permsOfFinset {α : Type u_1} [] (s : ) :

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

Equations
• One or more equations did not get rendered due to their size.
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 : ) :
().card = s.card.factorial
def fintypePerm {α : Type u_1} [] [] :

The collection of permutations of a fintype is a fintype.

Equations
Instances For
instance equivFintype {α : Type u_1} {β : Type u_2} [] [] [] [] :
Fintype (α β)
Equations
• One or more equations did not get rendered due to their size.
theorem Fintype.card_perm {α : Type u_1} [] [] :
= ().factorial
theorem Fintype.card_equiv {α : Type u_1} {β : Type u_2} [] [] [] [] (e : α β) :
Fintype.card (α β) = ().factorial