Theorems · Definition · group theory

Equiv.Perm.cycleFactorsAux

{α : Type u_2} →
  [DecidableEq α] →
    [Fintype α] →
      (l : List α) →
        (f : Equiv.Perm α) →
          (∀ {x : α}, f x ≠ x → x ∈ l) →
            { pl // pl.prod = f ∧ (∀ g ∈ pl, g.IsCycle) ∧ List.Pairwise Equiv.Perm.Disjoint pl }

Given a list l : List α and a permutation f : Perm α whose nonfixed points are all in l, recursively factors f into cycles.

Defined in

Mathlib.GroupTheory.Perm.Cycle.Factors

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqFintype