Cycle_Decomposition_of_Conjugate_v2
Provedconjugationcyclesgroup-theorypermutationsproofwiki
Let denote the symmetric group on letters. Let . The cycle decomposition of the permutation can be obtained from that of by replacing each in the cycle decomposition of with .
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.GroupTheory.Perm.Cycle.Type
Formal statement
theorem Cycle_Decomposition_of_Conjugate_v2 {α : Type _} [DecidableEq α] [Fintype α] (σ τ : Equiv.Perm α) : (σ * τ * σ⁻¹).cycleType = τ.cycleType := by sorrySource