K_Cycle_can_be_Factored_into_Transpositions_v2

Proved

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

cyclesgroup-theorypermutationsproofwikitranspositions

Every $k$ -cycle can be factorised into the product of $k - 1$ transpositions. This factorisation is not unique.

Preamble

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

Formal statement

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

Source

https://proofwiki.org/wiki/K-Cycle_can_be_Factored_into_Transpositions

View graph