Irreducible characters of degree coprime to p (source code)

= Irreducible characters of degree coprime to p
{title2=$\operatorname{Irr}_{p'}(G)$}

For a <finite group> $G$ and <prime number> $p$, the notation
$$
\operatorname{Irr}_{p'}(G)=\{\chi\in\operatorname{Irr}(G):p\nmid\chi(1)\}
$$
denotes the <irreducible characters> whose <irreducible character degree> is coprime to $p$.