Theorems · Definition · group theory

Equiv.Perm.swapFactorsAux

{α : Type u} →
  [inst : DecidableEq α] →
    (l : List α) → (f : Equiv.Perm α) → (∀ {x : α}, f x ≠ x → x ∈ l) → { l // l.prod = f ∧ ∀ g ∈ l, g.IsSwap }

Given a list l : List α and a permutation f : Perm α such that the nonfixed points of f are in l, recursively factors f as a product of transpositions.

Defined in

Mathlib.GroupTheory.Perm.Sign

Cited by

0 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEq