Theorems · Definition · group theory

Equiv.Perm.cycleFactors

{α : Type u_2} →
  [Fintype α] →
    [LinearOrder α] →
      (f : Equiv.Perm α) → { 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.

Defined in

Mathlib.GroupTheory.Perm.Cycle.Factors

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeLinearOrder