Existence_and_Uniqueness_of_Cycle_Decomposition_v2

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

cycle-decompositiongroup-theorypermutationsproofwiki

Let $S_n$ denote the symmetric group on $n$ letters. Every element of $S_n$ may be uniquely expressed as a cycle decomposition, up to the order of factors.

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.GroupTheory.Perm.Cycle.Type

Formal statement

theorem Existence_and_Uniqueness_of_Cycle_Decomposition_v2 {α : Type _} [DecidableEq α] [Fintype α] (σ : Equiv.Perm α) : ∃ l : List (Equiv.Perm α), (∀ c ∈ l, Equiv.Perm.IsCycle c) ∧ l.prod = σ := by sorry

Source

https://proofwiki.org/wiki/Existence_and_Uniqueness_of_Cycle_Decomposition

View graph