Sum of squares of irreducible degrees (source code)

= Sum of squares of irreducible degrees

If $\rho_1,\ldots,\rho_k$ are the complex irreducible representations of a finite group $G$ and $n_j=\dim\rho_j$, decomposition of the <regular representation> gives
$$
\sum_{j=1}^k n_j^2=|G|.
$$