Theorems · Theorem · group theory

AlternatingGroup.map_subtype_of_cycleType

∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (m : Multiset ℕ),
  Finset.map (Function.Embedding.subtype fun x => x ∈ alternatingGroup α) {g | (↑g).cycleType = m} =
    if Even (m.sum + m.card) then {g | g.cycleType = m} else ∅

Defined in

Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Cited by

3 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEq