mathlib3 documentation

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:

def perms_of_list {α : Type u_1} [decidable_eq α] :

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

Equations
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 α} :
f perms_of_list l {x : α}, f x x x l
theorem mem_perms_of_list_iff {α : Type u_1} [decidable_eq α] {l : list α} {f : equiv.perm α} :
f perms_of_list l {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 α} :
f perms_of_finset s {x : α}, f x x x s
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_equiv {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] [fintype α] [fintype β] (e : α β) :