Irreps collectively distinguish group elements

Let be entries of matrix representations of each irrep . Then the function subspace spanned by all such entries distinguishes all group elements in , where for any there exists a linear combination

such that and for . #m/thm/rep

Proof

This follows from the existence of the Regular group representation . For we can define

using the unnormalised inner product on , which has the required property, and since is a representation it is unitarily equivalent to a direct sum of irreps, i.e.

and so treating and as indices

as required.

#state/tidy | #lang/en | #SemBr