Documentation

Mathlib.Data.Fintype.Perm

Fintype instances for Equiv and Perm #

Main declarations:

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

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

Equations
Instances For
    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 xx l) :
    theorem mem_of_mem_permsOfList {α : Type u_1} [DecidableEq α] {l : List α} {f : Equiv.Perm α} :
    f permsOfList l∀ (x : α), f x xx l
    theorem mem_permsOfList_iff {α : Type u_1} [DecidableEq α] {l : List α} {f : Equiv.Perm α} :
    f permsOfList l ∀ {x : α}, f x xx l
    theorem nodup_permsOfList {α : Type u_1} [DecidableEq α] {l : List α} :
    l.Nodup(permsOfList l).Nodup
    def permsOfFinset {α : Type u_1} [DecidableEq α] (s : Finset α) :

    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
      theorem mem_perms_of_finset_iff {α : Type u_1} [DecidableEq α] {s : Finset α} {f : Equiv.Perm α} :
      f permsOfFinset s ∀ {x : α}, f x xx 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 α] :

      The collection of permutations of a fintype is a fintype.

      Equations
      Instances For
        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 α] :
        theorem Fintype.card_equiv {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [Fintype α] [Fintype β] (e : α β) :
        Fintype.card (α β) = (Fintype.card α).factorial