Theorems · Theorem · group theory

Equiv.Perm.centralizer_le_alternating_iff

∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {g : Equiv.Perm α},
  Subgroup.centralizer {g} ≤ alternatingGroup α ↔
    (∀ c ∈ g.cycleType, Odd c) ∧ Fintype.card α ≤ g.cycleType.sum + 1 ∧ ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1

The centralizer of a permutation is contained in the alternating group if and only if its cycles have odd length, with at most one of each, and there is at most one fixed point.

Defined in

Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEq