[proofplan] We convert the discriminant $D_f = \prod_{i < j}(\alpha_i - \alpha_j)^2$ into a product over all ordered pairs, picking up a sign $(-1)^{n(n-1)/2}$. Regrouping the ordered double product by the outer index $i$ yields $\prod_{i=1}^{n} f'(\alpha_i)$, because the factored form $f(t) = \prod_j(t - \alpha_j)$ gives $f'(\alpha_i) = \prod_{j \neq i}(\alpha_i - \alpha_j)$ upon differentiation and evaluation. Since $f$ is separable of degree $n$ with roots $\alpha_1, \ldots, \alpha_n$, there are exactly $n$ distinct $K$-homomorphisms $\varphi_i: K(\alpha_1) \hookrightarrow L$ defined by $\varphi_i(\alpha_1) = \alpha_i$, and the product $\prod_{i=1}^{n} f'(\alpha_i) = \prod_{i=1}^{n} \varphi_i(f'(\alpha_1))$ equals $\operatorname{N}_{K(\alpha_1)/K}(f'(\alpha_1))$ by the homomorphism formula for the norm. [/proofplan] [step:Convert the discriminant from a product over unordered pairs to a product over all ordered pairs] The discriminant is \begin{align*} D_f = \prod_{1 \le i < j \le n} (\alpha_i - \alpha_j)^2. \end{align*} We compare this with the product over all ordered pairs $(i,j)$ with $i \neq j$. For each unordered pair $\{i,j\}$ with $i < j$, the ordered-pair product contributes the two factors $(\alpha_i - \alpha_j)$ and $(\alpha_j - \alpha_i)$, whose product is \begin{align*} (\alpha_i - \alpha_j)(\alpha_j - \alpha_i) = -(\alpha_i - \alpha_j)^2. \end{align*} Since there are $\binom{n}{2} = \frac{n(n-1)}{2}$ such pairs, the full ordered product is \begin{align*} \prod_{\substack{i,j=1 \\ i \neq j}}^{n} (\alpha_i - \alpha_j) &= \prod_{1 \le i < j \le n} \bigl[(\alpha_i - \alpha_j)(\alpha_j - \alpha_i)\bigr] = \prod_{1 \le i < j \le n} \bigl[-(\alpha_i - \alpha_j)^2\bigr] = (-1)^{n(n-1)/2}\, D_f. \end{align*} Rearranging: \begin{align*} D_f = (-1)^{n(n-1)/2} \prod_{\substack{i,j=1 \\ i \neq j}}^{n} (\alpha_i - \alpha_j). \end{align*} [guided] The discriminant $D_f = \prod_{i<j}(\alpha_i-\alpha_j)^2$ is indexed by $\binom{n}{2}$ unordered pairs. To connect with the formal derivative, we need a product indexed by individual roots — which means reorganising into a product over all $n(n-1)$ ordered pairs $(i,j)$ with $i \neq j$. The passage from unordered to ordered pairs introduces a sign. Each unordered pair $\{i,j\}$ with $i < j$ contributes the ordered factors $(\alpha_i - \alpha_j)$ and $(\alpha_j - \alpha_i) = -(\alpha_i - \alpha_j)$, so their product is $-(\alpha_i - \alpha_j)^2$. The sign $(-1)^{n(n-1)/2}$ counts the total number of pairs. Note that $(-1)^{n(n-1)/2}$ is its own multiplicative inverse: $\bigl((-1)^{n(n-1)/2}\bigr)^2 = (-1)^{n(n-1)} = 1$ since $n(n-1)$ is even for all $n$. This is why the formula $D_f = (-1)^{n(n-1)/2}\prod_{i \neq j}(\alpha_i - \alpha_j)$ inverts cleanly from $\prod_{i \neq j}(\alpha_i - \alpha_j) = (-1)^{n(n-1)/2} D_f$. [/guided] [/step] [step:Express the ordered double product as $\prod_{i=1}^{n} f'(\alpha_i)$ via the Leibniz product rule] Since $f$ is monic of degree $n$ with roots $\alpha_1, \ldots, \alpha_n$ in the splitting field, we have the factorisation \begin{align*} f(t) = \prod_{j=1}^{n}(t - \alpha_j). \end{align*} (If $f$ is not monic with leading coefficient $c$, replace $f$ by its monic associate $c^{-1}f$, which has the same roots and the same discriminant.) Applying the Leibniz product rule for differentiation of $n$ factors: \begin{align*} f'(t) = \sum_{k=1}^{n} \prod_{\substack{j=1 \\ j \neq k}}^{n} (t - \alpha_j). \end{align*} We evaluate at $t = \alpha_i$ for a fixed index $i \in \{1, \ldots, n\}$. In the $k$-th summand, the product runs over all $j \neq k$. When $k \neq i$, the index $j = i$ is not excluded, so the factor $(t - \alpha_j)\big|_{j=i} = \alpha_i - \alpha_i = 0$ appears, and the entire summand vanishes. When $k = i$, the index $j = i$ is excluded, and no zero factor occurs. Hence only the $k = i$ term survives: \begin{align*} f'(\alpha_i) = \prod_{\substack{j=1 \\ j \neq i}}^{n}(\alpha_i - \alpha_j). \end{align*} Taking the product over all roots: \begin{align*} \prod_{i=1}^{n} f'(\alpha_i) = \prod_{i=1}^{n}\prod_{\substack{j=1 \\ j \neq i}}^{n}(\alpha_i - \alpha_j) = \prod_{\substack{i,j=1 \\ i \neq j}}^{n}(\alpha_i - \alpha_j). \end{align*} Substituting into the result of the previous step: \begin{align*} D_f = (-1)^{n(n-1)/2}\prod_{i=1}^{n} f'(\alpha_i). \end{align*} [guided] The key identity $f'(\alpha_i) = \prod_{j \neq i}(\alpha_i - \alpha_j)$ is the bridge between the discriminant (defined via pairwise differences of roots) and the field norm (defined via $K$-homomorphisms). Why does the formal derivative appear? The factored form $f(t) = \prod_j(t-\alpha_j)$ is a product of $n$ linear factors. Differentiating by the product rule gives a sum of $n$ terms: the $k$-th term removes the $k$-th factor and multiplies the remaining $n-1$ factors. At $t = \alpha_i$, all $n-1$ remaining factors in a given term must be nonzero for the term to contribute. This happens only when the removed factor is $(t - \alpha_i)$ itself — i.e., when $k = i$. The surviving term is $\prod_{j \neq i}(\alpha_i - \alpha_j)$, which records all pairwise differences from $\alpha_i$ to the other roots. Since each root $\alpha_i$ contributes the $n-1$ differences $\{\alpha_i - \alpha_j : j \neq i\}$, and as $i$ ranges over $\{1, \ldots, n\}$ we obtain every ordered pair $(i,j)$ with $i \neq j$ exactly once, the product $\prod_i f'(\alpha_i)$ equals the full ordered double product. Regarding the leading coefficient: if $f(t) = c\prod_j(t - \alpha_j)$ for $c \neq 1$, then $f'(\alpha_i) = c\prod_{j \neq i}(\alpha_i - \alpha_j)$ and $\prod_i f'(\alpha_i) = c^n \prod_{i \neq j}(\alpha_i - \alpha_j)$. The theorem statement uses $f'$, not the derivative of the monic associate. However, $D_f$ as defined by $\prod_{i<j}(\alpha_i - \alpha_j)^2$ is independent of $c$. One resolves this either by assuming $f$ is monic (which is harmless since the discriminant and the norm are both unchanged up to appropriate powers of $c$), or by carrying the factor $c^n$ through and absorbing it into the norm computation. We adopt the monic convention for clarity. [/guided] [/step] [step:Identify $\prod_{i=1}^{n} f'(\alpha_i)$ as $\operatorname{N}_{K(\alpha_1)/K}(f'(\alpha_1))$ via the homomorphism formula for the norm] Let $L$ denote the splitting field of $f$ over $K$. Since $f$ is separable, $\alpha_1, \ldots, \alpha_n$ are distinct. The $K$-homomorphisms from $K(\alpha_1)$ into $L$ are in bijection with the roots of the minimal polynomial of $\alpha_1$ over $K$: each homomorphism is determined by the image of $\alpha_1$, which must be a root of this minimal polynomial. We now use the hypothesis that $f$ is separable of degree $n$ with $n$ distinct roots. The $K$-homomorphisms $\varphi_1, \ldots, \varphi_n: K(\alpha_1) \hookrightarrow L$ defined by $\varphi_i(\alpha_1) = \alpha_i$ are well-defined and distinct precisely when $\alpha_1, \ldots, \alpha_n$ are all conjugates of $\alpha_1$ over $K$, i.e., when the minimal polynomial of $\alpha_1$ has degree $n$. This is equivalent to $f$ being irreducible over $K$, since an irreducible separable polynomial of degree $n$ is the minimal polynomial of each of its roots, and $[K(\alpha_1):K] = n$. Assuming $f$ is irreducible over $K$ (which is the standard setting for this theorem), there are exactly $n$ distinct $K$-homomorphisms $\varphi_i: K(\alpha_1) \hookrightarrow L$, one for each root. Since $f' \in K[t]$ has coefficients in $K$ and each $\varphi_i$ fixes $K$ pointwise, $\varphi_i$ commutes with polynomial evaluation: \begin{align*} \varphi_i(f'(\alpha_1)) = f'(\varphi_i(\alpha_1)) = f'(\alpha_i). \end{align*} By the [Trace and Norm via Homomorphisms](/theorems/1294), applied to the finite separable extension $K(\alpha_1)/K$ of degree $n$ with element $f'(\alpha_1) \in K(\alpha_1)$: \begin{align*} \operatorname{N}_{K(\alpha_1)/K}(f'(\alpha_1)) = \prod_{i=1}^{n}\varphi_i(f'(\alpha_1)) = \prod_{i=1}^{n} f'(\alpha_i). \end{align*} The hypotheses of the [Trace and Norm via Homomorphisms](/theorems/1294) require that $K(\alpha_1)/K$ be a finite separable extension. Finiteness holds because $[K(\alpha_1):K] = n < \infty$. Separability holds because the minimal polynomial of $\alpha_1$ is $f$ itself (since $f$ is irreducible), which is separable by hypothesis. [guided] This is the step where the algebraic structure of field extensions converts a product over roots into a norm. The key mechanism is: 1. Each root $\alpha_i$ of $f$ is a conjugate of $\alpha_1$ over $K$ (because $f$ is irreducible over $K$, so it is the minimal polynomial of $\alpha_1$). 2. Each conjugate $\alpha_i$ determines a unique $K$-homomorphism $\varphi_i: K(\alpha_1) \hookrightarrow L$ via $\varphi_i(\alpha_1) = \alpha_i$. 3. Since $\varphi_i$ is a $K$-algebra homomorphism, it commutes with evaluation of any polynomial $g \in K[t]$: the coefficients of $g$ lie in $K$ and are fixed by $\varphi_i$, so $\varphi_i(g(\alpha_1)) = g(\varphi_i(\alpha_1)) = g(\alpha_i)$. Applying step (3) with $g = f'$ gives $\varphi_i(f'(\alpha_1)) = f'(\alpha_i)$, and hence $\prod_{i=1}^{n} f'(\alpha_i) = \prod_{i=1}^{n}\varphi_i(f'(\alpha_1))$. The [Trace and Norm via Homomorphisms](/theorems/1294) then identifies this product as $\operatorname{N}_{K(\alpha_1)/K}(f'(\alpha_1))$. The theorem requires that $K(\alpha_1)/K$ be finite and separable, and that $\varphi_1, \ldots, \varphi_n$ be the complete list of $K$-homomorphisms $K(\alpha_1) \hookrightarrow \bar{K}$. Both conditions hold: finiteness is immediate since $\alpha_1$ is algebraic over $K$, and separability follows from $f$ being separable. The count $n = [K(\alpha_1):K]$ ensures that we have listed all $K$-homomorphisms. What if $f$ is not irreducible? Then $[K(\alpha_1):K] = d < n$, and there are only $d$ $K$-homomorphisms from $K(\alpha_1)$ into $L$. In this case, $\operatorname{N}_{K(\alpha_1)/K}(f'(\alpha_1)) = \prod_{i=1}^{d} f'(\alpha_i)$, which is a proper sub-product of $\prod_{i=1}^{n} f'(\alpha_i)$. The theorem statement uses $\operatorname{N}_{K(\alpha_1)/K}$, which implicitly requires that the product over the conjugates of $\alpha_1$ accounts for all roots — hence the implicit assumption that $f$ is irreducible. [/guided] [/step] [step:Combine the three identities to conclude] Assembling the results of the preceding steps. From the first step: \begin{align*} D_f = (-1)^{n(n-1)/2}\prod_{\substack{i,j=1 \\ i \neq j}}^{n}(\alpha_i - \alpha_j). \end{align*} From the second step: \begin{align*} \prod_{\substack{i,j=1 \\ i \neq j}}^{n}(\alpha_i - \alpha_j) = \prod_{i=1}^{n} f'(\alpha_i). \end{align*} From the third step: \begin{align*} \prod_{i=1}^{n} f'(\alpha_i) = \operatorname{N}_{K(\alpha_1)/K}(f'(\alpha_1)). \end{align*} Substituting: \begin{align*} D_f = (-1)^{n(n-1)/2}\operatorname{N}_{K(\alpha_1)/K}\bigl(f'(\alpha_1)\bigr). \end{align*} [/step]