TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

If $σ \in S_{n}$ has $c_{k}$ cycles of length $k$ , then $∣ C_{S_{n}} (σ) ∣ = \prod_{k = 1}^{n} k^{c_{k}} c_{k}!$

Statement

If $σ \in S_{n}$ has $c_{k}$ cycles of length $k$ , including fixed points when $k = 1$ , then $∣ C_{S_{n}} (σ) ∣ = \prod_{k = 1}^{n} k^{c_{k}} c_{k}! .$ The formula uses the empty product $1$ when $n = 0$ .

Facts & Assumptions

Given: A permutation $σ \in S_{n}$ of cycle type $(c_{1}, \dots, c_{n})$ .

[F1]

The centralizer consists of the permutations commuting with $σ$ (The conjugacy class ${Cl}_{G} (x)$ and centralizer $C_{G} (x)$ of an element).

[F2]

Every permutation has a disjoint-cycle decomposition unique up to reordering and cyclic rotation, and its cycle type counts the orbits of each length, including fixed points as $1$ -cycles (Every permutation of a finite set is a product of pairwise disjoint cycles, uniquely up to reordering and cyclic rotation, Support, fixed points, disjoint cycles, cycle length, disjoint-cycle decompositions, and cycle type).

[F3]

There are $c_{k}!$ bijections of a $c_{k}$ -element set (A finite set $A$ with $∣ A ∣ = n$ has exactly $n!$ bijections onto itself, and $n!$ bijections onto any set of the same cardinality).

[F4]

The cardinality of a finite product of finite choice sets is the product of their cardinalities, with the empty product having cardinality $1$ (The product rule: $∣ A \times B ∣ = ∣ A ∣ ∣ B ∣$ , and $∣ \prod_{i < m} A_{i} ∣ = \prod_{i < m} ∣ A_{i} ∣$ ).

Proof

technique · counting

1.1

If $g σ = σ g$ and $O$ is a $⟨ σ ⟩$ -orbit, then $g (O)$ is another orbit of the same size.

F1F2algebra

2.1

For the $c_{k}$ orbits of size $k$ , $g$ may permute those orbits in $c_{k}!$ ways by [F3]. Once a target orbit is chosen, the image of one marked point has $k$ choices, and commutation forces all other images; hence there are $k^{c_{k}} c_{k}!$ choices at length $k$ .

F1F2F3step 1.1

3.1

Conversely, arbitrary orbit permutations and cyclic offsets from step 2.1 assemble on the disjoint orbits to a unique bijection $g$ , and the forced-image rule makes $g σ = σ g$ .

F2step 2.1algebra

4.1

Choices for distinct lengths are independent, so [F4] and steps 2.1--3.1 give the displayed product. If $c_{k} = 0$ its factor is $k^{0} 0! = 1$ ; for the identity the result is $n!$ , and for $n = 0$ it is the empty product $1$ .

F3F4step 2.1step 3.1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 79 results over 20 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

D. A. Craven, Groups, Geometry and Representation Theory (standard reference, not scraped)
K. Conrad, Conjugacy Classes (standard reference, not scraped)

If σ∈Snσ∈Sn​ has ckck​ cycles of length kk, then ∣CSn(σ)∣=∏k=1nkckck!∣CSn​​(σ)∣=∏k=1n​kck​ck​!