Group_of_Permutations_either_All_or_Half_Even_v2

Proved

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

even-permutationsgroup-theoryparitypermutationsproofwiki

Let $G$ be a group of permutations. Then either ''exactly half'' of the permutations in $G$ are even, or they are ''all'' even.

Preamble

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

Formal statement

theorem Group_of_Permutations_either_All_or_Half_Even_v2 {α : Type _} [DecidableEq α] [Fintype α] (G : Subgroup (Equiv.Perm α)) [Fintype G] : (∀ g : G, Equiv.Perm.sign (g : Equiv.Perm α) = 1) ∨ 2 * (Finset.univ.filter (fun g : G => Equiv.Perm.sign (g : Equiv.Perm α) = 1)).card = Fintype.card G := by sorry

Source

https://proofwiki.org/wiki/Group_of_Permutations_either_All_or_Half_Even

View graph