permsOfList — Mathlib

English

PermsOfList assigns to any finite list l a list of all its permutations, as elements of the permutation group on α.

Русский

PermsOfList сопоставляет любой конечной списку l всю совокупность перестановок его элементов, как элементов группы перестановок над α.

LaTeX

$$$\\mathrm{permsOfList} : \\mathrm{List}(\\alpha) \\to \\mathrm{List}(\\mathrm{Perm}(\\alpha)).$$$

Lean4

/-- Given a list, produce a list of all permutations of its elements. -/
def permsOfList : List α → List (Perm α)
  | [] => [1]
  | a :: l => permsOfList l ++ l.flatMap fun b => (permsOfList l).map fun f => Equiv.swap a b * f

Похожие утверждения