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

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

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 α} : List.Nodup l → List.Nodup (permsOfList l)

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 α) : Finset.card (permsOfFinset s) = Nat.factorial (Finset.card s)

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 := (_ : ∀ (a : Equiv.Perm α), a ∈ permsOfFinset Finset.univ) }

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 α) = Nat.factorial (Fintype.card α)

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