Parity_of_K_Cycle_v2
Provedcyclesgroup-theoryparitypermutationsproofwiki
Let be a -cycle. Then Thus or equivalently
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.GroupTheory.Perm.Cycle.Type
Formal statement
theorem Parity_of_K_Cycle_v2 {α : Type _} [DecidableEq α] [Fintype α] (σ : Equiv.Perm α) (hσ : σ.IsCycle) : Equiv.Perm.sign σ = (-1) ^ (σ.support.card + 1) := by sorrySource