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:

source
def perms_of_list {α : Type u_1} [decidable_eq α] :
list α → list (equiv.perm α)

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

Equations
source
theorem length_perms_of_list {α : Type u_1} [decidable_eq α] (l : list α) :
(perms_of_list l).length = l.length.factorial
source
theorem mem_perms_of_list_of_mem {α : Type u_1} [decidable_eq α] {l : list α} {f : equiv.perm α} (h : ∀ (x : α), ⇑f x ≠ x → x ∈ l) :
f ∈ perms_of_list l
source
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
source
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
source
theorem nodup_perms_of_list {α : Type u_1} [decidable_eq α] {l : list α} (hl : l.nodup) :
(perms_of_list l).nodup
source
def perms_of_finset {α : Type u_1} [decidable_eq α] (s : finset α) :
finset (equiv.perm α)

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

Equations
source
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
source
theorem card_perms_of_finset {α : Type u_1} [decidable_eq α] (s : finset α) :
(perms_of_finset s).card = s.card.factorial
source
def fintype_perm {α : Type u_1} [decidable_eq α] [fintype α] :
fintype (equiv.perm α)

The collection of permutations of a fintype is a fintype.

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