Theorems · Theorem · group theory

Equiv.Perm.nat_card_centralizer

∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (g : Equiv.Perm α),
  Nat.card ↥(Subgroup.centralizer {g}) =
    (Fintype.card α - g.cycleType.sum).factorial * g.cycleType.prod *
      ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType).factorial

Cardinality of the centralizer in Equiv.Perm α of a permutation given cycleType

Defined in

Mathlib.GroupTheory.Perm.Centralizer

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEqFintype