Theorems · Theorem · group theory

alternatingGroup.mem_kleinFour_of_order_two_pow

∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α],
  Nat.card α = 4 →
    ∀ {g : Equiv.Perm α}, g ∈ alternatingGroup α → ∀ {n : ℕ}, orderOf g ∣ 2 ^ n → g.cycleType = ∅ ∨ g.cycleType = {2, 2}

Defined in

Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Cited by

1 results in Mathlib

Foundations

Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqFintype