Theorems · Theorem · group theory

AlternatingGroup.card_of_cycleType_mul_eq

∀ (α : Type u_1) [inst : Fintype α] [inst_1 : DecidableEq α] (m : Multiset ℕ),
  {g | (↑g).cycleType = m}.card *
      ((Fintype.card α - m.sum).factorial * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m).factorial) =
    if (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card) then (Fintype.card α).factorial else 0

The cardinality of even permutations of given cycleType

Defined in

Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEq