Positive-degree norm-one virtual characters are irreducible (source code)

= Positive-degree norm-one virtual characters are irreducible
{title2=$\langle\psi,\psi\rangle=1,\ \psi(1)>0\Longrightarrow\psi\in\operatorname{Irr}(G)$}

Write the <virtual character> as $\psi=\sum_\chi a_\chi\chi$ with integer coefficients and <irreducible characters> $\chi$. <Character orthogonality> gives $\langle\psi,\psi\rangle=\sum_\chi a_\chi^2$. Norm one forces exactly one coefficient to be $1$ or $-1$, and positive degree selects the positive sign.