The Weyl dimension formula

Given: The Axiom of Choice, a dominant integral weight $\lambda \in {\mathrm{\Lambda }}^{+}$, the finite-dimensional simple module $L(\lambda )$ with its multiplicities, the Weyl vector $\rho$, the positive system ${\mathrm{\Phi }}^{+}$ and the form $(,)$ on $E={\mathrm{span}}_{\mathbb{R}}\mathrm{\Phi }$.

The Axiom of Choice is assumed; it enters through the regularized evaluation of [F1] and its suppliers (The Axiom of Choice).

For every $t>0$ one has ${\sum }_{\mu }{m}_{\lambda }(\mu )e^{2t(\mu ,\rho )}={\prod }_{\alpha \in {\mathrm{\Phi }}^{+}}(e^{t(\lambda +\rho ,\alpha )}-e^{-t(\lambda +\rho ,\alpha )})/{\prod }_{\alpha \in {\mathrm{\Phi }}^{+}}(e^{t(\rho ,\alpha )}-e^{-t(\rho ,\alpha )})$; the left side is a finite sum of exponentials, continuous at $t=0$ with value ${\sum }_{\mu }{m}_{\lambda }(\mu )=\dim L(\lambda )$, and the right side has the finite limit ${\prod }_{\alpha \in {\mathrm{\Phi }}^{+}}(\lambda +\rho ,\alpha )\mathrm{/}(\rho ,\alpha )$ as $t\to 0+$ (Regularized evaluation of the Weyl character quotient at one).

A function defined for $t>0$ has at most one limit as $t\to 0+$ (The $\epsilon$-$\delta$ limit ${\lim }_{x\to c}f(x)=L$ of $f:A\to \mathbb{R}$ at a limit point $c$ of $A$).

For every $\nu \in E$ and every root $\alpha$ one has $(\nu ,\alpha )=\frac{(\alpha ,\alpha )}{2}⟨\nu ,{\alpha }^{\vee }⟩$, because ${\alpha }^{\vee }=2\alpha \mathrm{/}(\alpha ,\alpha )$ after identifying $E$ with its dual by the form; moreover $⟨\rho ,{\alpha }^{\vee }⟩>0$ and $⟨\lambda +\rho ,{\alpha }^{\vee }⟩>0$ for every positive root $\alpha$ (Finite Weyl root system, lattice and chamber conventions, Positive coroot pairings of a dominant integral weight, The Weyl vector rho for a chosen positive system).