Theorems · Theorem · group theory

Equiv.Perm.card_isConj_mul_eq

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

Defined in

Mathlib.GroupTheory.Perm.Centralizer

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEqFintype