[proofplan] We express the trace using the embeddings formula: for a finite separable extension $L/K$ of degree $n$, the $n$ distinct $K$-embeddings $\varphi_1, \ldots, \varphi_n \colon L \hookrightarrow \bar{K}$ give $\operatorname{Tr}_{L/K}(\alpha) = \sum_{i=1}^{n} \varphi_i(\alpha)$ for all $\alpha \in L$. The trace vanishes identically if and only if the $K$-linear combination $\varphi_1 + \cdots + \varphi_n$ is the zero function on $L$. By the [Linear Independence of Characters](/theorems/1282), distinct field homomorphisms from $L$ into a field are linearly independent over that field. This forces the sum to be nonzero, so there must exist $\alpha \in L$ with $\operatorname{Tr}_{L/K}(\alpha) \neq 0$. [/proofplan] [step:Express the trace as a sum of the $K$-embeddings $\varphi_1, \ldots, \varphi_n$] Let $n := [L : K]$. Since $L/K$ is a finite separable extension, it admits exactly $n$ distinct $K$-algebra homomorphisms into an algebraic closure $\bar{K}$ of $K$: \begin{align*} \varphi_1, \ldots, \varphi_n \colon L \hookrightarrow \bar{K}. \end{align*} Each $\varphi_i$ is a field homomorphism (hence injective) that restricts to the identity on $K$. The count $n = [L : K]$ is precisely the separable degree, which equals the full degree because $L/K$ is separable. By the [Trace and Norm via Homomorphisms](/theorems/1294), for every $\alpha \in L$: \begin{align*} \operatorname{Tr}_{L/K}(\alpha) = \sum_{i=1}^{n} \varphi_i(\alpha). \end{align*} [guided] The trace of an element $\alpha \in L$ over $K$ is defined as the trace of the $K$-linear map $m_\alpha \colon L \to L$ given by multiplication by $\alpha$: $\operatorname{Tr}_{L/K}(\alpha) = \operatorname{tr}(m_\alpha)$. While this definition is intrinsic (requiring no choice of algebraic closure), the embeddings formula provides a concrete and useful expression. Why exactly $n$ embeddings? A finite extension $L/K$ of degree $n$ has at most $n$ distinct $K$-embeddings into $\bar{K}$, with equality if and only if $L/K$ is separable. This is the defining property of separability for finite extensions: the number of distinct $K$-embeddings equals the degree. The hypothesis that $L/K$ is separable is consumed here to guarantee that we get the full count of $n$ distinct embeddings. The [Trace and Norm via Homomorphisms](/theorems/1294) then identifies the abstract linear-algebraic trace $\operatorname{tr}(m_\alpha)$ with the sum $\sum_{i=1}^{n} \varphi_i(\alpha)$. This reformulation transforms the problem from linear algebra (showing a certain linear map has nonzero trace) into a question about linear independence of field homomorphisms. [/guided] [/step] [step:Suppose for contradiction that the trace vanishes identically on $L$] Assume that $\operatorname{Tr}_{L/K}(\alpha) = 0$ for every $\alpha \in L$. By the embeddings formula established in the previous step, this means \begin{align*} \sum_{i=1}^{n} \varphi_i(\alpha) = 0 \quad \text{for all } \alpha \in L. \end{align*} Equivalently, the map $\varphi_1 + \cdots + \varphi_n \colon L \to \bar{K}$, defined by $\alpha \mapsto \sum_{i=1}^{n} \varphi_i(\alpha)$, is the zero function. Expressing this as a $\bar{K}$-linear dependence relation among the $\varphi_i$: the coefficients $c_1 = c_2 = \cdots = c_n = 1 \in \bar{K}$ (not all zero, since $n \ge 1$ and $1 \neq 0$) satisfy \begin{align*} \sum_{i=1}^{n} c_i \, \varphi_i(\alpha) = 0 \quad \text{for all } \alpha \in L, \end{align*} which is a nonzero $\bar{K}$-linear combination of $\varphi_1, \ldots, \varphi_n$ that vanishes identically on $L$. [/step] [step:Apply the Linear Independence of Characters to obtain a contradiction] The $K$-embeddings $\varphi_1, \ldots, \varphi_n \colon L \hookrightarrow \bar{K}$ are distinct field homomorphisms from the field $L$ into the field $\bar{K}$. By the [Linear Independence of Characters](/theorems/1282) (Dedekind's lemma on the linear independence of distinct field homomorphisms), distinct field homomorphisms $\varphi_1, \ldots, \varphi_n \colon L \to \bar{K}$ are linearly independent over $\bar{K}$. We verify the hypotheses of [Theorem 1282](/theorems/1282): we require that $\varphi_1, \ldots, \varphi_n$ are pairwise distinct field homomorphisms from a field $L$ into a field $E$. The $\varphi_i$ are distinct $K$-embeddings (distinct by the separability count), $L$ is a field (given), and $\bar{K}$ is a field (algebraic closures are fields). All hypotheses are satisfied. The conclusion of [Theorem 1282](/theorems/1282) states: if $c_1, \ldots, c_n \in \bar{K}$ satisfy $\sum_{i=1}^{n} c_i \, \varphi_i(\alpha) = 0$ for all $\alpha \in L$, then $c_1 = c_2 = \cdots = c_n = 0$. However, the previous step produced such a relation with $c_1 = c_2 = \cdots = c_n = 1 \neq 0$. This is a contradiction. [guided] The [Linear Independence of Characters](/theorems/1282) (due to Dedekind) asserts that distinct field homomorphisms from a field $L$ into a field $E$ are linearly independent as elements of the $E$-vector space of all functions from $L$ to $E$. Concretely: if $\varphi_1, \ldots, \varphi_n \colon L \to E$ are pairwise distinct field homomorphisms and $c_1, \ldots, c_n \in E$ satisfy $\sum_{i} c_i \varphi_i = 0$ (as a function $L \to E$), then every $c_i = 0$. Why does this apply here? Our $\varphi_1, \ldots, \varphi_n$ are distinct $K$-embeddings of $L$ into $\bar{K}$. Every $K$-embedding is in particular a field homomorphism (it is a ring homomorphism between fields, hence injective, and it preserves the identity). The distinctness comes from separability: a separable extension of degree $n$ has exactly $n$ distinct $K$-embeddings into any algebraically closed extension, and these are pairwise distinct by definition. The contradiction is immediate: the assumption that the trace vanishes identically produced a nonzero linear combination (with all coefficients equal to $1 \in \bar{K}$) of distinct field homomorphisms that equals the zero function. Since $1 \neq 0$ in $\bar{K}$ (and $n \ge 1$, so the combination is nonzero), this violates Dedekind's lemma. It is worth noting the contrast with the inseparable case. For an inseparable extension $L/K$ in characteristic $p > 0$, the [Inseparable Extensions Have Vanishing Trace](/theorems/1295) shows that $\operatorname{Tr}_{L/K}(\alpha) = 0$ for all $\alpha \in L$. The embeddings formula still holds, but the number of distinct embeddings is strictly less than $[L : K]$: each embedding is repeated $[L : K]_{\mathrm{insep}}$ times (the inseparable degree), so the sum becomes $[L : K]_{\mathrm{insep}} \cdot \sum_{j} \varphi_j(\alpha)$ where the sum runs over only the $[L : K]_{\mathrm{sep}}$ distinct embeddings. If $\operatorname{char} K = p$ divides the inseparable degree (as it must when the extension is truly inseparable), the factor $[L : K]_{\mathrm{insep}}$ is zero in $K$, killing the entire sum. Separability eliminates this collapse. [/guided] [/step] [step:Conclude that the trace is non-vanishing] The assumption that $\operatorname{Tr}_{L/K}(\alpha) = 0$ for all $\alpha \in L$ led to a contradiction with the [Linear Independence of Characters](/theorems/1282). Therefore, there exists $\alpha \in L$ with $\operatorname{Tr}_{L/K}(\alpha) \neq 0$. [/step]