Specht modules classify the complex irreducibles of $S_n$

Given: $n\ge 0$. Let ${\mathcal{P}}_n$ be the set of partitions of $n$, ${\mathcal{C}}_n$ the set of conjugacy classes of $S_n$, and ${\mathcal{I}}_n$ the set of isomorphism classes of finite-dimensional irreducible complex $S_n$-representations.

A partition is a finite weakly decreasing list of positive integers with sum $n$ (Partitions, English diagrams, and conjugation).

$S_n=\mathrm{Sym}(\{1,\dots ,n\})$ and $S_0=\mathrm{Sym}(\mathrm{\varnothing })=\{1\}$ (Partitions, English diagrams, and conjugation, The symmetric group $\mathrm{Sym}(X)$: the bijections of a set $X$ under composition); $\mathrm{Sym}(X)$ is a group ($\mathrm{Sym}(X)$ is a group under composition, and it is non-abelian whenever $X$ has at least three distinct elements).

$S_n$ is finite and $\mathrm{\mid }{S}_n\mathrm{\mid }=n!$ (The Lehmer code gives $\mathrm{\mid }{S}_n\mathrm{\mid }=n!$ again).

$\mathbb{C}=\mathbb{R}[x]\mathrm{/}(x^2+1)$ is a field containing the embedded copy $\iota :\mathbb{R}\hookrightarrow \mathbb{C}$ (The complex numbers as $\mathbb{R}[x]\mathrm{/}(x^2+1)$, with the real embedding and imaginary unit $i$, $\mathbb{C}=\mathbb{R}[x]\mathrm{/}(x^2+1)$ is a field, every element is uniquely $a+bi$, and every nonzero element has inverse $(a-bi)\mathrm{/}(a^2+b^2)$); this field embedding preserves $1$ and addition (Field homomorphism and embedding).

$\mathbb{R}$ is an ordered field and, for every integer $m\ge 1$, its canonical natural $m\cdot 1_{\mathbb{R}}$ is positive (The reals form a totally ordered field, Canonical naturals are positive and strictly increasing).

A ring has characteristic zero exactly when no positive integer multiple of its identity is zero (The characteristic of a ring is the additive order of $1_R$, with $0$ recording infinite order; $n\cdot 1_R=0$ holds exactly when $\mathrm{char}(R)\mid n$; and in an integral domain every nonzero element has the same additive order as $1_R$).

The natural-to-integer embedding preserves order, and zero divides no positive integer (The naturals embed in the integers, Invertibility of a positive natural scalar in a field).

$\mathbb{C}$ is algebraically closed (The complex numbers are algebraically closed).

For a finite group $G$ and algebraically closed field $k$ with $\mathrm{char}k\nmid \mathrm{\mid }G\mathrm{\mid }$, the finite set of irreducible representation classes has cardinality equal to the finite set of conjugacy classes (If $k$ is algebraically closed and $\mathrm{char}k\nmid \mathrm{\mid }G\mathrm{\mid }$, the number of irreducible representations of $G$ equals the number of conjugacy classes).

Conjugacy classes of $S_n$ are in bijection with the tuples of nonnegative integers $(c_1,\dots ,c_n)$ satisfying ${\sum }_{k=1}^{n}k{c}_k=n$; when $n=0$ the unique empty tuple indexes the identity class (The conjugacy classes of $S_n$ are indexed by the tuples $(c_1,\dots ,c_n)$ with $\sum k{c}_k=n$).

Each $S^{\lambda }$ is a nonzero irreducible complex representation of $S_n$ (Complex Specht modules are irreducible).

If $S^{\lambda }\cong S^{\mu }$ for $\lambda ,\mu ⊢n$, then $\lambda =\mu$ (Distinct complex Specht modules are inequivalent).

A representation is finite-dimensional as specified in A finite-dimensional representation $\rho :G\to \mathrm{GL}(V)$ over a field, and its degree, is irreducible when it is nonzero and has no proper nonzero subrepresentation (Subrepresentations, direct sums of representations, and irreducibility), and two representations are equivalent exactly when an invertible intertwiner exists (Intertwiners, the spaces ${\mathrm{Hom}}_G(V,W)$ and ${\mathrm{End}}_G(V)$, equivalent representations, and faithful representations).

For finite sets, a bijection transports cardinality (The cardinality $\mid A\mid$ of a finite set).

If $J\subseteq I$ and $I$ is finite, then $J$ is finite and $\mathrm{\mid }J\mathrm{\mid }=\mathrm{\mid }I\mathrm{\mid }$ implies $J=I$ (A subset of a finite set is finite, with $\mid B\mid \le \mid A\mid$, and equality holds if and only if $B=A$).

A map is injective when equal outputs force equal inputs, is surjective when its image is the codomain, and is bijective when it is both injective and surjective (Injection, surjection, bijection).

For $n=0$ the only partition is the empty list (Partitions, English diagrams, and conjugation).

Cardinality is defined for finite sets, and a finite set has cardinality only as a natural number (The cardinality $\mid A\mid$ of a finite set).

For $n=0$, the unique empty tuple indexes the identity class of $S_0$ (The conjugacy classes of $S_n$ are indexed by the tuples $(c_1,\dots ,c_n)$ with $\sum k{c}_k=n$).

A finite set has cardinality zero exactly when it is empty (The cardinality $\mid A\mid$ of a finite set).

No Axiom of Choice is used.