Conjugate_Permutations_have_Same_Cycle_Type_v2

Proved

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

conjugationcycle-typegroup-theorypermutationsproofwiki

Let $n \ge 1$ be a natural number. Let $G$ be a subgroup of the symmetric group on $n$ letters $S_n$ . Let $\sigma, \rho \in G$ . Then $\sigma$ and $\rho$ are conjugate they have the same cycle type.

Preamble

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

Formal statement

theorem Conjugate_Permutations_have_Same_Cycle_Type_v2 {α : Type _} [DecidableEq α] [Fintype α] (σ τ : Equiv.Perm α) (h : IsConj σ τ) : σ.cycleType = τ.cycleType := by sorry

Source

https://proofwiki.org/wiki/Conjugate_Permutations_have_Same_Cycle_Type

View graph