# `Fintype` instances for `Equiv` and `Perm` #

Main declarations:

- `permsOfFinset s`: The finset of permutations of the finset `s`.

source
def permsOfList {α : Type u_1} [DecidableEq α] :
List α → List (Equiv.Perm α)

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

Equations

- permsOfList [] = [1]
- permsOfList (a :: l) = permsOfList l ++ List.flatMap (fun (b : α) => List.map (fun (f : Equiv.Perm α) => Equiv.swap a b * f) (permsOfList l)) l

Instances For

source
theorem length_permsOfList {α : Type u_1} [DecidableEq α] (l : List α) :
(permsOfList l).length = l.length.factorial
source
theorem mem_permsOfList_of_mem {α : Type u_1} [DecidableEq α] {l : List α} {f : Equiv.Perm α} (h : ∀ (x : α), f x ≠ x → x ∈ l) :
f ∈ permsOfList l
source
theorem mem_of_mem_permsOfList {α : Type u_1} [DecidableEq α] {l : List α} {f : Equiv.Perm α} :
f ∈ permsOfList l → ∀ {x : α}, f x ≠ x → x ∈ l
source
theorem mem_permsOfList_iff {α : Type u_1} [DecidableEq α] {l : List α} {f : Equiv.Perm α} :
f ∈ permsOfList l ↔ ∀ {x : α}, f x ≠ x → x ∈ l
source
theorem nodup_permsOfList {α : Type u_1} [DecidableEq α] {l : List α} :
l.Nodup → (permsOfList l).Nodup
source
def permsOfFinset {α : Type u_1} [DecidableEq α] (s : Finset α) :
Finset (Equiv.Perm α)

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

source
theorem mem_perms_of_finset_iff {α : Type u_1} [DecidableEq α] {s : Finset α} {f : Equiv.Perm α} :
f ∈ permsOfFinset s ↔ ∀ {x : α}, f x ≠ x → x ∈ s
source
theorem card_perms_of_finset {α : Type u_1} [DecidableEq α] (s : Finset α) :
(permsOfFinset s).card = s.card.factorial
source
def fintypePerm {α : Type u_1} [DecidableEq α] [Fintype α] :
Fintype (Equiv.Perm α)

The collection of permutations of a fintype is a fintype.

Equations

- fintypePerm = { elems := permsOfFinset Finset.univ, complete := ⋯ }

Instances For

source
instance Equiv.instFintype {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [Fintype α] [Fintype β] :
Fintype (α ≃ β)
Equations

- One or more equations did not get rendered due to their size.

source
instance MulEquiv.instFintype {α : Type u_4} {β : Type u_5} [Mul α] [Mul β] [DecidableEq α] [DecidableEq β] [Fintype α] [Fintype β] :
Fintype (α ≃* β)
Equations

- One or more equations did not get rendered due to their size.

source
instance AddEquiv.instFintype {α : Type u_4} {β : Type u_5} [Add α] [Add β] [DecidableEq α] [DecidableEq β] [Fintype α] [Fintype β] :
Fintype (α ≃+ β)
Equations

- One or more equations did not get rendered due to their size.

source
theorem Fintype.card_perm {α : Type u_1} [DecidableEq α] [Fintype α] :
card (Equiv.Perm α) = (card α).factorial
source
theorem Fintype.card_equiv {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [Fintype α] [Fintype β] (e : α ≃ β) :
card (α ≃ β) = (card α).factorial