Parity_of_Inverse_of_Permutation_v2

Proved

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

group-theoryinverseparitypermutationsproofwiki

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

Preamble

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

Formal statement

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

Source

https://proofwiki.org/wiki/Parity_of_Inverse_of_Permutation

View graph