Theorems · Definition · group theory

Equiv.Perm.truncCycleFactors

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

Factors a permutation f into a list of disjoint cyclic permutations that multiply to f, without a linear order.

Defined in

Mathlib.GroupTheory.Perm.Cycle.Factors

Cited by

3 results in Mathlib

Foundations

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

Assumes

DecidableEqFintype