of T on the complexified Lie algebra of K. The root system R has all the usual properties of a root system, except that the elements of R may not span . We then choose a base for R and we say that an integral element is dominant if for all . Finally, we say that one weight is higher than another if their difference can be expressed as a linear combination of elements of with non-negative coefficients. The irreducible finite-dimensional representations of K are then classified by a theorem of the highest weight, which is closely related to the analogous theorem classifying representations of a semisimple Lie algebra. The result says that: every irreducible representation has highest weight, the highest weight is always a dominant, analytically integral element, two irreducible representations with the same highest weight are isomorphic, and every dominant, analytically integral element arises as the highest weight of an irreducible representation. The theorem of the highest weight for representations of K is then almost the same as for semisimple Lie algebras, with one notable exception: The concept of an integral element is different. The weights of a representation are analytically integral in the sense described in the previous subsection. Every analytically integral element is integral in the Lie algebra sense, but not the other way around. (This phenomenon reflects that, in general, not every representation of the Lie algebra comes from a representation of the group K.) On the other hand, if K is simply connected, the set of possible highest weights in the group sense is the same as the set of possible highest weights in the Lie algebra sense. The Weyl character formula If is representation of K, we define the character of to be the function given by . This function is easily seen to be a class function, i.e., for all and in K. Thus, is determined by its restriction to T. The study of characters is an important part of the representation theory of compact groups. One crucial result, which is a corollary of the Peter–Weyl theorem, is that the characters form an orthonormal basis for the set of square-integrable class functions in K. A second key result is the Weyl character formula, which gives an explicit formula for the character—or, rather, the restriction of the character to T—in terms of the highest weight of the representation. In the closely related representation