Parity_of_Conjugate_of_Permutation_v2

Proved

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

conjugationgroup-theoryparitypermutationsproofwiki

Let $S_n$ denote the symmetric group on $n$ letters. Then $\forall \pi, \rho \in S_n: \map \sgn {\pi \rho \pi^{-1} } = \map \sgn \rho$ where $\map \sgn \pi$ is the sign of $\pi$ .

Preamble

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

Formal statement

theorem Parity_of_Conjugate_of_Permutation_v2 {α : Type _} [DecidableEq α] [Fintype α] (π ρ : Equiv.Perm α) : Equiv.Perm.sign (π * ρ * π⁻¹) = Equiv.Perm.sign ρ := by sorry

Source

https://proofwiki.org/wiki/Parity_of_Conjugate_of_Permutation

View graph