card_isConj_eq — Mathlib

English

The number of permutations with a fixed cycleType m equals a product depending on m and card α.

Русский

Число перестановок с фиксированным cycleType m равно произведению, зависящему от m и размера α.

LaTeX

$$card_of_cycleType$$

Lean4

/-- Cardinality of a conjugacy class in `Equiv.Perm α` of a given `cycleType` -/
theorem card_isConj_eq :
    Nat.card {h : Perm α | IsConj g h} =
      (Fintype.card α)! /
        ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
          (∏ n ∈ g.cycleType.toFinset, (g.cycleType.count n)!)) :=
  by
  rw [← card_isConj_mul_eq g, Nat.div_eq_of_eq_mul_left _]
  ·
    rfl
      -- This is the cardinal of the centralizer

  · rw [← nat_card_centralizer g]
    apply Nat.card_pos

Похожие утверждения