[proofplan] We start from the Weyl character formula and compute the value of the character at the identity by a one-parameter specialization of the group algebra. The numerator and denominator alternants both vanish at the identity, so the main point is to identify their first nonzero Taylor terms. The [Weyl denominator formula](/theorems/9382) computes the denominator leading term, while the general anti-invariant polynomial factorization shows that the numerator leading term has the same universal constant, with $\rho$ replaced by $\lambda+\rho$. Dividing the leading terms gives the stated product. [/proofplan]

[step:Specialize the Weyl character formula along a regular one-parameter path]Let $E\subset\mathfrak h^*$ denote the real [vector space](/page/Vector%20Space) spanned by $\Phi$, and let $W$ denote the Weyl group of $\Phi$. Let $N:=|\Phi^+|$. Choose an element $H\in\mathfrak h$ such that \begin{align*} \alpha(H)\ne 0 \end{align*} for every $\alpha\in\Phi$; such an $H$ exists because $\mathfrak h$ is not the finite union of the root hyperplanes $\ker\alpha$. For each $\mu\in\mathfrak h^*$, define the one-parameter specialization \begin{align*} s_\mu:\mathbb C\to\mathbb C \end{align*} by \begin{align*} s_\mu(t):=\exp(t\mu(H)). \end{align*} This induces a specialization of formal exponentials by sending $e^\mu$ to $s_\mu(t)$. The hypotheses of the Weyl character formula [citetheorem:9384] are satisfied: $\mathfrak g$ is a finite-dimensional complex semisimple [Lie algebra](/page/Lie%20Algebra), $\mathfrak h$ is a Cartan subalgebra, $\Phi^+$ is the chosen positive root system, $\lambda\in P^+$ is dominant integral, and $L(\lambda)$ is the irreducible finite-dimensional highest-weight module of highest weight $\lambda$. Therefore \begin{align*} \operatorname{ch}L(\lambda)=\frac{A_{\lambda+\rho}}{A_\rho}, \end{align*} where, for $\xi\in\mathfrak h^*$, \begin{align*} A_\xi:=\sum_{w\in W}\det(w)e^{w\xi}. \end{align*} After applying the specialization, define \begin{align*} F_\xi:\mathbb C\to\mathbb C \end{align*} by \begin{align*} F_\xi(t):=\sum_{w\in W}\det(w)\exp(t(w\xi)(H)). \end{align*} For each $\mu\in\mathfrak h^*$, define the $\mu$-weight space of $L(\lambda)$ by \begin{align*} L(\lambda)_\mu:=\{v\in L(\lambda): h\cdot v=\mu(h)v\text{ for every }h\in\mathfrak h\}. \end{align*} Define the specialized character \begin{align*} \operatorname{ch}_t L(\lambda):=\sum_{\mu\in\mathfrak h^*}\dim L(\lambda)_\mu\exp(t\mu(H)). \end{align*} The sum is finite because $L(\lambda)$ is finite-dimensional. Then, for all sufficiently small $t$ for which $F_\rho(t)\ne 0$, \begin{align*} \operatorname{ch}_t L(\lambda)=\frac{F_{\lambda+\rho}(t)}{F_\rho(t)}. \end{align*} Since $L(\lambda)$ is finite-dimensional and \begin{align*} \operatorname{ch}_t L(\lambda)=\sum_{\mu\in\mathfrak h^*}\dim L(\lambda)_\mu\exp(t\mu(H)) \end{align*} with only finitely many nonzero weight spaces, the specialization satisfies \begin{align*} \lim_{t\to 0}\operatorname{ch}_t L(\lambda)=\sum_{\mu\in\mathfrak h^*}\dim L(\lambda)_\mu=\dim L(\lambda). \end{align*} Therefore \begin{align*} \dim L(\lambda)=\lim_{t\to 0}\frac{F_{\lambda+\rho}(t)}{F_\rho(t)}, \end{align*} provided the limit of the quotient is computed from the leading Taylor terms.[/step]

[guided]For each $\mu\in\mathfrak h^*$, the $\mu$-weight space of $L(\lambda)$ is \begin{align*} L(\lambda)_\mu:=\{v\in L(\lambda): h\cdot v=\mu(h)v\text{ for every }h\in\mathfrak h\}. \end{align*} The character is a finite formal sum because $L(\lambda)$ is finite-dimensional: \begin{align*} \operatorname{ch}L(\lambda)=\sum_{\mu\in\mathfrak h^*}\dim L(\lambda)_\mu e^\mu. \end{align*} To recover the ordinary dimension from this character, we want to set every formal exponential $e^\mu$ equal to $1$. The specialization $e^\mu\mapsto \exp(t\mu(H))$ does exactly that in the limit $t\to 0$, because $\exp(t\mu(H))\to 1$ for every weight $\mu$. We choose $H\in\mathfrak h$ with $\alpha(H)\ne 0$ for every root $\alpha$ so that the denominator leading term will not vanish. Such an element exists because the forbidden set is the finite union of the proper hyperplanes $\ker\alpha\subset\mathfrak h$. The Weyl character formula [citetheorem:9384] applies because $\mathfrak g$ is finite-dimensional complex semisimple, $\mathfrak h$ is a Cartan subalgebra, $\Phi^+$ is the chosen positive root system, $\lambda\in P^+$ is dominant integral, and $L(\lambda)$ is the irreducible finite-dimensional highest-weight module of highest weight $\lambda$. It gives \begin{align*} \operatorname{ch}L(\lambda)=\frac{A_{\lambda+\rho}}{A_\rho}, \end{align*} where \begin{align*} A_\xi=\sum_{w\in W}\det(w)e^{w\xi}. \end{align*} After specialization, this becomes the quotient of the analytic functions \begin{align*} F_{\lambda+\rho}(t)=\sum_{w\in W}\det(w)\exp(t(w(\lambda+\rho))(H)) \end{align*} and \begin{align*} F_\rho(t)=\sum_{w\in W}\det(w)\exp(t(w\rho)(H)). \end{align*} Define the specialized character by \begin{align*} \operatorname{ch}_t L(\lambda):=\sum_{\mu\in\mathfrak h^*}\dim L(\lambda)_\mu\exp(t\mu(H)). \end{align*} Because the Weyl character formula is an identity in the group algebra of formal exponentials, applying the specialization sends its numerator and denominator to $F_{\lambda+\rho}(t)$ and $F_\rho(t)$, respectively. Thus \begin{align*} \operatorname{ch}_t L(\lambda)=\frac{F_{\lambda+\rho}(t)}{F_\rho(t)} \end{align*} where the quotient is defined. Finally, because only finitely many weights occur in $L(\lambda)$, we can pass to the limit term by term: \begin{align*} \lim_{t\to 0}\operatorname{ch}_t L(\lambda)=\sum_{\mu\in\mathfrak h^*}\dim L(\lambda)_\mu=\dim L(\lambda). \end{align*} So the dimension problem has been reduced to computing \begin{align*} \lim_{t\to 0}\frac{F_{\lambda+\rho}(t)}{F_\rho(t)}. \end{align*} The rest of the proof identifies the first nonzero Taylor coefficient of each alternant.[/guided]

[step:Compute the leading term of the denominator alternant]By the Weyl denominator formula [citetheorem:9382], \begin{align*} A_\rho=e^\rho\prod_{\alpha\in\Phi^+}(1-e^{-\alpha}). \end{align*} After specialization, this gives \begin{align*} F_\rho(t)=\exp(t\rho(H))\prod_{\alpha\in\Phi^+}\left(1-\exp(-t\alpha(H))\right). \end{align*} For each $\alpha\in\Phi^+$, Taylor expansion at $t=0$ gives \begin{align*} 1-\exp(-t\alpha(H))=t\alpha(H)+O(t^2). \end{align*} Also \begin{align*} \exp(t\rho(H))=1+O(t). \end{align*} Multiplying the $N$ factors gives \begin{align*} F_\rho(t)=t^N\prod_{\alpha\in\Phi^+}\alpha(H)+O(t^{N+1}). \end{align*} Since $\alpha(H)\ne 0$ for every $\alpha\in\Phi^+$, the coefficient \begin{align*} \prod_{\alpha\in\Phi^+}\alpha(H) \end{align*} is nonzero. Hence $F_\rho$ vanishes to exact order $N$ at $t=0$.[/step]

[guided]We apply the Weyl denominator formula [citetheorem:9382] to the root system $\Phi$ with the chosen positive system $\Phi^+$. Its hypotheses match the present setting because $\Phi$ is the finite reduced crystallographic root system attached to the complex semisimple Lie algebra $\mathfrak g$ and $\Phi^+$ has already been chosen. The formula gives \begin{align*} A_\rho=e^\rho\prod_{\alpha\in\Phi^+}(1-e^{-\alpha}). \end{align*} Under the specialization $e^\mu\mapsto\exp(t\mu(H))$, this becomes \begin{align*} F_\rho(t)=\exp(t\rho(H))\prod_{\alpha\in\Phi^+}\left(1-\exp(-t\alpha(H))\right). \end{align*} We now compute the first nonzero Taylor term. For each fixed positive root $\alpha\in\Phi^+$, the ordinary Taylor expansion of the exponential function at $0$ gives \begin{align*} \exp(-t\alpha(H))=1-t\alpha(H)+O(t^2). \end{align*} Therefore \begin{align*} 1-\exp(-t\alpha(H))=t\alpha(H)+O(t^2). \end{align*} Also \begin{align*} \exp(t\rho(H))=1+O(t). \end{align*} Multiplying the $N=|\Phi^+|$ factors, the unique contribution of order $t^N$ is obtained by taking the linear term $t\alpha(H)$ from every positive-root factor and the constant term $1$ from $\exp(t\rho(H))$. Hence \begin{align*} F_\rho(t)=t^N\prod_{\alpha\in\Phi^+}\alpha(H)+O(t^{N+1}). \end{align*} The choice of $H$ was regular, meaning $\alpha(H)\ne0$ for every root $\alpha\in\Phi$. In particular each factor $\alpha(H)$ with $\alpha\in\Phi^+$ is nonzero, so \begin{align*} \prod_{\alpha\in\Phi^+}\alpha(H)\ne0. \end{align*} Thus the denominator alternant $F_\rho$ vanishes to exact order $N$ at $t=0$, and its leading coefficient is precisely $\prod_{\alpha\in\Phi^+}\alpha(H)$.[/guided]

[step:Identify the leading term of a general Weyl alternant]For $\xi\in\mathfrak h^*$, expand $F_\xi$ at $t=0$: \begin{align*} F_\xi(t)=\sum_{m=0}^{\infty}\frac{t^m}{m!}B_m(\xi), \end{align*} where \begin{align*} B_m(\xi):=\sum_{w\in W}\det(w)\bigl((w\xi)(H)\bigr)^m. \end{align*} For each $m$, the function \begin{align*} B_m:\mathfrak h^*\to\mathbb C \end{align*} is a [homogeneous polynomial](/page/Homogeneous%20Polynomial) of degree $m$ in $\xi$. Moreover, for every $u\in W$, \begin{align*} B_m(u\xi)=\det(u)B_m(\xi), \end{align*} because the substitution $w'=wu$ gives \begin{align*} B_m(u\xi)=\sum_{w\in W}\det(w)\bigl((wu\xi)(H)\bigr)^m=\det(u)\sum_{w'\in W}\det(w')\bigl((w'\xi)(H)\bigr)^m. \end{align*} Thus $B_m$ is $W$-anti-invariant. For each root $\alpha\in\Phi$, let $s_\alpha\in W$ denote the reflection across the hyperplane $\{\xi\in\mathfrak h^*:\xi(\alpha^\vee)=0\}$. Let \begin{align*} D:\mathfrak h^*\to\mathbb C \end{align*} be the polynomial \begin{align*} D(\xi):=\prod_{\alpha\in\Phi^+}\xi(\alpha^\vee). \end{align*} Every $W$-anti-invariant polynomial is divisible by $D$: if $p$ is $W$-anti-invariant, then $p(s_\alpha\xi)=-p(\xi)$, so $p$ vanishes on the reflecting hyperplane $\{\xi:\xi(\alpha^\vee)=0\}$, and therefore the linear factor $\xi(\alpha^\vee)$ divides $p$ by the elementary [factor theorem](/theorems/3235). The coordinate ring of the finite-dimensional vector space $\mathfrak h^*$ is a [polynomial ring](/page/Polynomial%20Ring) over $\mathbb C$, hence a unique factorization domain. For distinct positive roots $\alpha$ and $\beta$, the coroots $\alpha^\vee$ and $\beta^\vee$ are not proportional in a reduced root system, so the linear forms $\xi\mapsto\xi(\alpha^\vee)$ and $\xi\mapsto\xi(\beta^\vee)$ are non-associate irreducible factors. Therefore their product $D$ divides $p$. Since $D$ has degree $N$, it follows that \begin{align*} B_m=0 \end{align*} for all $m<N$. For $m=N$, the same divisibility and degree comparison imply that there is a scalar $c_H\in\mathbb C$ such that \begin{align*} B_N(\xi)=c_HD(\xi) \end{align*} for every $\xi\in\mathfrak h^*$. Evaluating this identity at $\xi=\rho$ and comparing with the leading term of $F_\rho$ from the previous step gives \begin{align*} \frac{1}{N!}B_N(\rho)=\prod_{\alpha\in\Phi^+}\alpha(H). \end{align*} Hence \begin{align*} c_H=N!\frac{\prod_{\alpha\in\Phi^+}\alpha(H)}{\prod_{\alpha\in\Phi^+}\rho(\alpha^\vee)}. \end{align*} Consequently, for every regular $\xi\in\mathfrak h^*$, \begin{align*} F_\xi(t)=t^N\left(\prod_{\alpha\in\Phi^+}\alpha(H)\right)\left(\prod_{\alpha\in\Phi^+}\frac{\xi(\alpha^\vee)}{\rho(\alpha^\vee)}\right)+O(t^{N+1}). \end{align*}[/step]

[guided]We now explain why every alternant has its first possible nonzero term in degree $N=|\Phi^+|$. The Taylor coefficient of degree $m$ in \begin{align*} F_\xi(t)=\sum_{w\in W}\det(w)\exp(t(w\xi)(H)) \end{align*} is \begin{align*} \frac{1}{m!}B_m(\xi), \end{align*} where \begin{align*} B_m(\xi)=\sum_{w\in W}\det(w)\bigl((w\xi)(H)\bigr)^m. \end{align*} This is a homogeneous polynomial of degree $m$ in $\xi$. The crucial structural fact is that $B_m$ is anti-invariant under the Weyl group. Indeed, for $u\in W$, \begin{align*} B_m(u\xi)=\sum_{w\in W}\det(w)\bigl((wu\xi)(H)\bigr)^m. \end{align*} Using the change of index $w'=wu$, we have $\det(w)=\det(w')\det(u)$, and therefore \begin{align*} B_m(u\xi)=\det(u)\sum_{w'\in W}\det(w')\bigl((w'\xi)(H)\bigr)^m=\det(u)B_m(\xi). \end{align*} Now define \begin{align*} D(\xi):=\prod_{\alpha\in\Phi^+}\xi(\alpha^\vee). \end{align*} This polynomial has degree $N$. We claim that every $W$-anti-invariant polynomial is divisible by $D$. To see this, let $p:\mathfrak h^*\to\mathbb C$ be a $W$-anti-invariant polynomial. For the reflection $s_\alpha$ associated to $\alpha$, anti-invariance says \begin{align*} p(s_\alpha\xi)=-p(\xi). \end{align*} If $\xi$ lies on the reflecting hyperplane $\xi(\alpha^\vee)=0$, then $s_\alpha\xi=\xi$, so \begin{align*} p(\xi)=-p(\xi). \end{align*} Thus $p(\xi)=0$ on that hyperplane. Since $\xi\mapsto \xi(\alpha^\vee)$ is a linear defining equation for the hyperplane, the polynomial $p$ is divisible by that linear form. For distinct positive roots $\alpha$ and $\beta$, the linear forms $\xi\mapsto\xi(\alpha^\vee)$ and $\xi\mapsto\xi(\beta^\vee)$ are not scalar multiples, because $\alpha^\vee$ and $\beta^\vee$ are not proportional unless $\alpha=\beta$ in a reduced root system. Hence these linear factors are pairwise non-associate irreducible factors in the polynomial ring on $\mathfrak h^*$. Applying this to every positive root shows that $p$ is divisible by \begin{align*} D(\xi)=\prod_{\alpha\in\Phi^+}\xi(\alpha^\vee). \end{align*} Applying this to $p=B_m$, we get $D\mid B_m$. If $m<N$, then $B_m$ has degree smaller than $D$, so $B_m=0$. If $m=N$, then $B_N$ and $D$ have the same degree, hence \begin{align*} B_N(\xi)=c_HD(\xi) \end{align*} for some scalar $c_H$ depending on the chosen regular element $H$. We determine $c_H$ by evaluating at $\xi=\rho$. From the Weyl denominator formula computed in the previous step, \begin{align*} F_\rho(t)=t^N\prod_{\alpha\in\Phi^+}\alpha(H)+O(t^{N+1}). \end{align*} On the other hand, the Taylor expansion gives \begin{align*} F_\rho(t)=\frac{t^N}{N!}B_N(\rho)+O(t^{N+1}). \end{align*} Therefore \begin{align*} \frac{1}{N!}B_N(\rho)=\prod_{\alpha\in\Phi^+}\alpha(H). \end{align*} Since \begin{align*} B_N(\rho)=c_H\prod_{\alpha\in\Phi^+}\rho(\alpha^\vee), \end{align*} we obtain \begin{align*} c_H=N!\frac{\prod_{\alpha\in\Phi^+}\alpha(H)}{\prod_{\alpha\in\Phi^+}\rho(\alpha^\vee)}. \end{align*} Substituting this value of $c_H$ into the degree-$N$ Taylor term gives, for every regular $\xi$, \begin{align*} F_\xi(t)=t^N\left(\prod_{\alpha\in\Phi^+}\alpha(H)\right)\left(\prod_{\alpha\in\Phi^+}\frac{\xi(\alpha^\vee)}{\rho(\alpha^\vee)}\right)+O(t^{N+1}). \end{align*} This is the precise leading-term comparison needed for the quotient.[/guided]

[step:Apply the leading-term comparison to $\lambda+\rho$ and take the quotient]Let $\Delta\subset\Phi^+$ denote the set of simple roots. Because $\lambda\in P^+$, we have $\lambda(\beta^\vee)\in\mathbb Z_{\ge0}$ for every $\beta\in\Delta$. For every positive root $\alpha\in\Phi^+$, the positive coroot $\alpha^\vee$ is a nonnegative integral linear combination of the simple coroots: \begin{align*} \alpha^\vee=\sum_{\beta\in\Delta}n_{\alpha,\beta}\beta^\vee \end{align*} with coefficients $n_{\alpha,\beta}\in\mathbb Z_{\ge0}$, not all zero. Therefore \begin{align*} \lambda(\alpha^\vee)=\sum_{\beta\in\Delta}n_{\alpha,\beta}\lambda(\beta^\vee)\in\mathbb Z_{\ge0}. \end{align*} For each simple root $\beta\in\Delta$, the identity $s_\beta\rho=\rho-\beta$ gives $\rho(\beta^\vee)=1$. Hence, using the same coroot expansion, \begin{align*} \rho(\alpha^\vee)=\sum_{\beta\in\Delta}n_{\alpha,\beta}\rho(\beta^\vee)=\sum_{\beta\in\Delta}n_{\alpha,\beta}>0. \end{align*} Hence \begin{align*} (\lambda+\rho)(\alpha^\vee)=\lambda(\alpha^\vee)+\rho(\alpha^\vee)>0, \end{align*} so $\lambda+\rho$ is regular and none of the factors in the numerator product vanishes. Applying the leading-term formula with $\xi=\lambda+\rho$ gives \begin{align*} F_{\lambda+\rho}(t)=t^N\left(\prod_{\alpha\in\Phi^+}\alpha(H)\right)\left(\prod_{\alpha\in\Phi^+}\frac{(\lambda+\rho)(\alpha^\vee)}{\rho(\alpha^\vee)}\right)+O(t^{N+1}). \end{align*} The denominator computation gives \begin{align*} F_\rho(t)=t^N\prod_{\alpha\in\Phi^+}\alpha(H)+O(t^{N+1}). \end{align*} Since $\prod_{\alpha\in\Phi^+}\alpha(H)\ne 0$, division of these two expansions yields \begin{align*} \lim_{t\to 0}\frac{F_{\lambda+\rho}(t)}{F_\rho(t)} = \prod_{\alpha\in\Phi^+}\frac{(\lambda+\rho)(\alpha^\vee)}{\rho(\alpha^\vee)}. \end{align*} Combining this limit with the specialization identity from the first step, we obtain \begin{align*} \dim L(\lambda)=\prod_{\alpha\in\Phi^+}\frac{(\lambda+\rho)(\alpha^\vee)}{\rho(\alpha^\vee)}. \end{align*} This is the Weyl dimension formula.[/step]

[guided]We now apply the leading-term formula to the specific weight $\xi=\lambda+\rho$. First we check that no numerator factor vanishes. Let $\Delta\subset\Phi^+$ be the simple root set. Since $\lambda\in P^+$, we have $\lambda(\beta^\vee)\in\mathbb Z_{\ge0}$ for every $\beta\in\Delta$. If $\alpha\in\Phi^+$, then the positive coroot $\alpha^\vee$ is a nonnegative integral linear combination of the simple coroots: \begin{align*} \alpha^\vee=\sum_{\beta\in\Delta}n_{\alpha,\beta}\beta^\vee \end{align*} with $n_{\alpha,\beta}\in\mathbb Z_{\ge0}$ and at least one coefficient nonzero. Hence \begin{align*} \lambda(\alpha^\vee)=\sum_{\beta\in\Delta}n_{\alpha,\beta}\lambda(\beta^\vee)\ge0. \end{align*} Also $s_\beta\rho=\rho-\beta$ for a simple reflection $s_\beta$, so $\rho(\beta^\vee)=1$ for every $\beta\in\Delta$. Therefore \begin{align*} \rho(\alpha^\vee)=\sum_{\beta\in\Delta}n_{\alpha,\beta}\rho(\beta^\vee)=\sum_{\beta\in\Delta}n_{\alpha,\beta}>0. \end{align*} Combining the two inequalities gives \begin{align*} (\lambda+\rho)(\alpha^\vee)>0 \end{align*} for every $\alpha\in\Phi^+$, so $\lambda+\rho$ is regular. The leading-term formula from the previous step gives \begin{align*} F_{\lambda+\rho}(t)=t^N\left(\prod_{\alpha\in\Phi^+}\alpha(H)\right)\left(\prod_{\alpha\in\Phi^+}\frac{(\lambda+\rho)(\alpha^\vee)}{\rho(\alpha^\vee)}\right)+O(t^{N+1}). \end{align*} The denominator computation gives \begin{align*} F_\rho(t)=t^N\prod_{\alpha\in\Phi^+}\alpha(H)+O(t^{N+1}). \end{align*} The coefficient $\prod_{\alpha\in\Phi^+}\alpha(H)$ is nonzero because $H$ was chosen outside every root hyperplane. Dividing the two Taylor expansions therefore gives \begin{align*} \lim_{t\to0}\frac{F_{\lambda+\rho}(t)}{F_\rho(t)}=\prod_{\alpha\in\Phi^+}\frac{(\lambda+\rho)(\alpha^\vee)}{\rho(\alpha^\vee)}. \end{align*} The first step identified $\dim L(\lambda)$ with this limit of specialized characters. Substituting the computed limit yields \begin{align*} \dim L(\lambda)=\prod_{\alpha\in\Phi^+}\frac{(\lambda+\rho)(\alpha^\vee)}{\rho(\alpha^\vee)}. \end{align*} This is exactly the Weyl dimension formula.[/guided]