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

The collection of permutations of a fintype is a fintype.

Equations
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.
@[deprecated Equiv.instFintype (since := "2024-11-19")]
def equivFintype {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] [Fintype α] [Fintype β] :
Fintype (α β)

Alias of Equiv.instFintype.

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