Parity_Function_is_Homomorphism_v2
Provedgroup-theoryhomomorphismsparitypermutationsproofwiki
Let denote the symmetric group on letters. Let . Let be the sign of . Let the parity function of be defined as Parity of The mapping , where is the cyclic group of order 2, is a homomorphism.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.GroupTheory.Perm.Cycle.Type
Formal statement
theorem Parity_Function_is_Homomorphism_v2 {α : Type _} [DecidableEq α] [Fintype α] (σ τ : Equiv.Perm α) : Equiv.Perm.sign (σ * τ) = Equiv.Perm.sign σ * Equiv.Perm.sign τ := by sorrySource