Fintype instances for Equiv and Perm

Main declarations:

• permsOfFinset s: The finset of permutations of the finset s.

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 ++ l.bind fun (b : α) => List.map (fun (f : Equiv.Perm α) => Equiv.swap a b * f) (permsOfList l)

theorem length_permsOfList {α : Type u_1} [DecidableEq α] (l : List α) : (permsOfList l).length = l.length.factorial

theorem mem_permsOfList_of_mem {α : Type u_1} [DecidableEq α] {l : List α} {f : Equiv.Perm α} (h : ∀ (x : α), f x ≠ x → x ∈ l) : f ∈ permsOfList l

theorem mem_of_mem_permsOfList {α : Type u_1} [DecidableEq α] {l : List α} {f : Equiv.Perm α} : f ∈ permsOfList l → ∀ (x : α), f x ≠ x → x ∈ l

theorem mem_permsOfList_iff {α : Type u_1} [DecidableEq α] {l : List α} {f : Equiv.Perm α} : f ∈ permsOfList l ↔ ∀ {x : α}, f x ≠ x → x ∈ l

theorem nodup_permsOfList {α : Type u_1} [DecidableEq α] {l : List α} : l.Nodup → (permsOfList l).Nodup

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.

theorem mem_perms_of_finset_iff {α : Type u_1} [DecidableEq α] {s : Finset α} {f : Equiv.Perm α} : f ∈ permsOfFinset s ↔ ∀ {x : α}, f x ≠ x → x ∈ s

theorem card_perms_of_finset {α : Type u_1} [DecidableEq α] (s : Finset α) : (permsOfFinset s).card = s.card.factorial

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 := ⋯ }

instance equivFintype {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [Fintype α] [Fintype β] : Fintype (α ≃ β)

Equations

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

theorem Fintype.card_perm {α : Type u_1} [DecidableEq α] [Fintype α] : Fintype.card (Equiv.Perm α) = (Fintype.card α).factorial

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