Alphabeta Math
CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck 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.

The class equation of Sn is n!=∑∑kck=nn!/∏kkckck!

Statement

For every n≥0, n!=∑c1,…,cn≥0∑k=1nkck=nn!∏k=1nkckck!. When n=0, the one empty tuple contributes 1.

Facts & Assumptions

Given: The symmetric group Sn for n≥0.

[F1]

Conjugacy classes of Sn are indexed by the tuples with ∑kck=n (The conjugacy classes of Sn are indexed by the tuples (c1,…,cn) with ∑kck=n).

[F2]

A permutation of type (ck) has centralizer cardinality ∏kckck! (If σ∈Sn has ck cycles of length k, then ∣CSn(σ)∣=∏k=1nkckck!).

[F3]

A conjugacy class has cardinality ∣Cl⁡G(x)∣=[G:CG(x)] (G/CG(x)→Cl⁡G(x) is a bijection, so ∣Cl⁡G(x)∣=[G:CG(x)] whenever these cardinalities are finite), and ∣G∣=[G:H] ∣H∣ for H≤G (Lagrange's theorem: ∣G∣=[G:H]∣H∣ for every subgroup H of a finite group G), so the class size is ∣G∣/∣CG(x)∣.

[F4]

If x1,…,xr represent the non-singleton conjugacy classes of a finite group G, then ∣G∣=∣Z(G)∣+∑i[G:CG(xi)] (The class equation ∣G∣=∣Z(G)∣+∑i[G:CG(xi)] for a finite group).

Proof

technique · counting
1.1

By [F1], index the conjugacy classes by the displayed tuples.

F1
2.1

For a tuple (ck), [F2], [F3], and [F5] give class size n!/∏kckck!.

F2F3F5step 1.1
3.1

In [F4], the central term counts the singleton conjugacy classes and the sum counts every remaining class. Thus summing the sizes from step 2.1 and using [F5] for ∣Sn∣ gives the displayed identity.

F4F5step 1.1step 2.1
4.1

At n=0, [F1] gives the one empty type and all empty products and 0! equal 1, so the same formula reads 1=1.

F1F2F5∎

Depends on

Used by

Dependency tree · two levels

33 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources