[proofplan] We establish the setup, prove the extension is Galois, and compute its Galois group. Let $K$ be a field, let $L = K(x_1, \ldots, x_n)$ be the rational function field in $n$ independent indeterminates, and let $F = K(u_1, \ldots, u_n)$ where $u_1, \ldots, u_n$ are the elementary symmetric polynomials in $x_1, \ldots, x_n$. The general polynomial $f(t) = \prod_{i=1}^n (t - x_i)$ lies in $F[t]$ and splits completely over $L$, making $L$ a splitting field of $f$ over $F$. Since $f$ has $n$ distinct roots (the $x_i$ are independent indeterminates), $f$ is separable, so $L/F$ is Galois by the splitting-field characterisation. Each permutation $\sigma \in S_n$ acts on $L$ by permuting the indeterminates $x_i \mapsto x_{\sigma(i)}$, fixing $F$ pointwise (since the elementary symmetric polynomials are invariant under all permutations). This gives an injection $S_n \hookrightarrow \operatorname{Gal}(L/F)$. Applying [Artin's Lemma](/theorems/1272) to the subgroup $S_n \subset \operatorname{Aut}(L)$, we obtain $[L : L^{S_n}] = |S_n| = n!$. Since $F \subset L^{S_n}$ and also $[L : F] \le n!$ (because $f$ has degree $n$), a degree comparison forces $F = L^{S_n}$ and $|\operatorname{Gal}(L/F)| = n!$, so the injection is an isomorphism. [/proofplan]

[step:Identify $L$ as a splitting field of the general polynomial over $F$]Let $K$ be a field and let $x_1, \ldots, x_n$ be independent indeterminates over $K$. Define the rational function field $L := K(x_1, \ldots, x_n)$. The elementary symmetric polynomials in $x_1, \ldots, x_n$ are \begin{align*} u_1 &:= x_1 + x_2 + \cdots + x_n, \\ u_2 &:= \sum_{1 \le i < j \le n} x_i x_j, \\ &\;\;\vdots \\ u_k &:= \sum_{1 \le i_1 < \cdots < i_k \le n} x_{i_1} \cdots x_{i_k}, \\ &\;\;\vdots \\ u_n &:= x_1 x_2 \cdots x_n. \end{align*} Set $F := K(u_1, \ldots, u_n) \subset L$. By Vieta's formulas, the polynomial \begin{align*} f(t) := \prod_{i=1}^n (t - x_i) = t^n - u_1 t^{n-1} + u_2 t^{n-2} - \cdots + (-1)^n u_n \end{align*} has coefficients in $F$ and splits completely over $L$ with roots $x_1, \ldots, x_n$. Since $L = K(x_1, \ldots, x_n) = F(x_1, \ldots, x_n)$, the field $L$ is generated over $F$ by the roots of $f$. Therefore $L$ is a splitting field of $f$ over $F$.[/step]

[guided]The general polynomial is constructed by working backwards from its roots. We begin with $n$ independent indeterminates $x_1, \ldots, x_n$ over $K$ and form the rational function field $L = K(x_1, \ldots, x_n)$. The key insight is that the coefficients of the polynomial $\prod_{i=1}^n(t - x_i)$ are, up to sign, the elementary symmetric polynomials in $x_1, \ldots, x_n$. Define the elementary symmetric polynomials $u_1, \ldots, u_n$ as above and set $F = K(u_1, \ldots, u_n)$. Expanding the product $\prod_{i=1}^n(t - x_i)$ and collecting powers of $t$, we obtain \begin{align*} \prod_{i=1}^n (t - x_i) &= t^n - \left(\sum_i x_i\right) t^{n-1} + \left(\sum_{i < j} x_i x_j\right) t^{n-2} - \cdots + (-1)^n x_1 \cdots x_n \\ &= t^n - u_1 t^{n-1} + u_2 t^{n-2} - \cdots + (-1)^n u_n. \end{align*} Each coefficient $(-1)^k u_k$ lies in $F$, so $f(t) \in F[t]$. By construction, $f$ splits completely over $L$ with roots $x_1, \ldots, x_n$. Moreover, $L = F(x_1, \ldots, x_n)$: the inclusion $F(x_1, \ldots, x_n) \subset L$ holds because $F \subset L$ and each $x_i \in L$, and the reverse inclusion $L = K(x_1, \ldots, x_n) \subset F(x_1, \ldots, x_n)$ holds because $K \subset F$. Therefore $L$ is the splitting field of $f$ over $F$. Why does this matter? The splitting-field structure is what allows us to access the Galois machinery. Every automorphism of $L$ fixing $F$ must permute the roots of $f$, which constrains $\operatorname{Gal}(L/F)$ to be a subgroup of $S_n$.[/guided]

[step:Show that $f$ is separable and conclude $L/F$ is Galois]The roots of $f$ are $x_1, \ldots, x_n$, which are distinct elements of $L$ (they are independent indeterminates and hence pairwise unequal in $L$). A polynomial with pairwise distinct roots in its splitting field is separable. Since $L$ is the splitting field of the separable polynomial $f \in F[t]$, the extension $L/F$ is Galois by the [Splitting Fields of Separable Polynomials Are Galois](/theorems/1271) theorem.[/step]

[guided]We must verify that $f$ has no repeated roots. The roots of $f$ in $L$ are $x_1, \ldots, x_n$. Since $x_1, \ldots, x_n$ are algebraically independent indeterminates over $K$, they are in particular pairwise distinct elements of $L$. (If $x_i = x_j$ held for some $i \ne j$, then $x_i - x_j = 0$ would be a polynomial relation of degree one among the indeterminates, contradicting algebraic independence.) A polynomial is separable if and only if it has no repeated roots in its splitting field. Since the $n$ roots $x_1, \ldots, x_n$ are pairwise distinct, $f$ is separable. We now invoke the [Splitting Fields of Separable Polynomials Are Galois](/theorems/1271) theorem. The hypotheses are: (i) $f \in F[t]$ is separable, and (ii) $L$ is the splitting field of $f$ over $F$. Both conditions have been verified. The conclusion is that $L/F$ is a Galois extension, i.e., $L/F$ is finite, separable, and normal, and $|\operatorname{Gal}(L/F)| = [L : F]$. Note that this argument is characteristic-free: we do not need $\operatorname{char} K = 0$ for separability, because the distinctness of the roots is guaranteed by the algebraic independence of the indeterminates, not by a derivative computation.[/guided]

[step:Construct an injection $S_n \hookrightarrow \operatorname{Gal}(L/F)$ from the permutation action on indeterminates]Each permutation $\sigma \in S_n$ defines a $K$-algebra automorphism \begin{align*} \varphi_\sigma: L = K(x_1, \ldots, x_n) &\to K(x_1, \ldots, x_n) = L \\ x_i &\mapsto x_{\sigma(i)} \end{align*} extended to $L$ by the universal property of the rational function field: $\varphi_\sigma$ acts on a rational function $g(x_1, \ldots, x_n)/h(x_1, \ldots, x_n)$ by permuting the variables according to $\sigma$. Since the $x_i$ are independent indeterminates, $\varphi_\sigma$ is a well-defined field automorphism of $L$. We claim $\varphi_\sigma$ fixes $F = K(u_1, \ldots, u_n)$ pointwise. It suffices to show $\varphi_\sigma(u_k) = u_k$ for each $k = 1, \ldots, n$, since $\varphi_\sigma$ fixes $K$ and the $u_k$ generate $F$ over $K$. For each $k$, \begin{align*} \varphi_\sigma(u_k) &= \varphi_\sigma\!\left(\sum_{1 \le i_1 < \cdots < i_k \le n} x_{i_1} \cdots x_{i_k}\right) = \sum_{1 \le i_1 < \cdots < i_k \le n} x_{\sigma(i_1)} \cdots x_{\sigma(i_k)}. \end{align*} Since $\sigma$ is a bijection of $\{1, \ldots, n\}$, the set $\{\sigma(i_1), \ldots, \sigma(i_k)\}$ ranges over all $k$-element subsets of $\{1, \ldots, n\}$ as $\{i_1, \ldots, i_k\}$ does. Therefore the sum on the right equals $u_k$. This holds for every $k$, so $\varphi_\sigma$ fixes each $u_k$, hence fixes $F$ pointwise. Therefore $\varphi_\sigma \in \operatorname{Gal}(L/F)$. The map \begin{align*} \varphi: S_n &\to \operatorname{Gal}(L/F) \\ \sigma &\mapsto \varphi_\sigma \end{align*} is a group homomorphism: for all $\sigma, \tau \in S_n$ and each $i \in \{1, \ldots, n\}$, \begin{align*} \varphi_{\sigma \circ \tau}(x_i) = x_{(\sigma \circ \tau)(i)} = x_{\sigma(\tau(i))} = \varphi_\sigma(x_{\tau(i)}) = \varphi_\sigma(\varphi_\tau(x_i)) = (\varphi_\sigma \circ \varphi_\tau)(x_i). \end{align*} Since the $x_i$ generate $L$ over $K$, $\varphi_{\sigma \circ \tau} = \varphi_\sigma \circ \varphi_\tau$. The homomorphism $\varphi$ is injective: if $\varphi_\sigma = \operatorname{id}_L$, then $x_{\sigma(i)} = x_i$ for all $i$, so $\sigma(i) = i$ for all $i$ (since distinct indeterminates are distinct elements of $L$), giving $\sigma = \operatorname{id}$. Therefore $\varphi$ is an injection $S_n \hookrightarrow \operatorname{Gal}(L/F)$.[/step]

[guided]The idea is that permuting the roots of $f$ should give automorphisms of the splitting field $L$, and that the elementary symmetric polynomials should be invariant under all such permutations. For each $\sigma \in S_n$, we define the automorphism $\varphi_\sigma$ by $x_i \mapsto x_{\sigma(i)}$. Because $x_1, \ldots, x_n$ are algebraically independent over $K$, there is no polynomial relation among them. Consequently, any permutation of the indeterminates extends to a well-defined $K$-algebra automorphism of $K[x_1, \ldots, x_n]$ (by the universal property of polynomial rings), and this extends uniquely to the fraction field $L = K(x_1, \ldots, x_n)$. Does $\varphi_\sigma$ fix $F$? The field $F = K(u_1, \ldots, u_n)$ is generated over $K$ by the elementary symmetric polynomials. The defining property of $u_k$ is that it is a sum over all $k$-element subsets: \begin{align*} u_k = \sum_{1 \le i_1 < \cdots < i_k \le n} x_{i_1} \cdots x_{i_k}. \end{align*} Applying $\varphi_\sigma$ replaces each $x_{i_j}$ by $x_{\sigma(i_j)}$. Since $\sigma$ is a bijection of $\{1, \ldots, n\}$, the collection of $k$-element subsets $\{\sigma(i_1), \ldots, \sigma(i_k)\}$ is a re-enumeration of the same collection of $k$-element subsets of $\{1, \ldots, n\}$. Therefore \begin{align*} \varphi_\sigma(u_k) = \sum_{1 \le i_1 < \cdots < i_k \le n} x_{\sigma(i_1)} \cdots x_{\sigma(i_k)} = u_k. \end{align*} Since $\varphi_\sigma$ fixes $K$ (it is a $K$-algebra map) and fixes each generator $u_k$ of $F$ over $K$, it fixes $F$ pointwise. To verify that $\sigma \mapsto \varphi_\sigma$ is a group homomorphism: the composition $\varphi_\sigma \circ \varphi_\tau$ sends $x_i$ to $\varphi_\sigma(x_{\tau(i)}) = x_{\sigma(\tau(i))} = x_{(\sigma \circ \tau)(i)}$, which is the same as $\varphi_{\sigma \circ \tau}(x_i)$. Since the $x_i$ generate $L$, the two automorphisms agree on all of $L$. To verify injectivity: if $\varphi_\sigma = \operatorname{id}_L$, then $x_{\sigma(i)} = x_i$ for each $i$. Since distinct indeterminates are distinct elements of $L$ (they are algebraically independent and in particular pairwise unequal), $\sigma(i) = i$ for all $i$, so $\sigma = \operatorname{id}$. We therefore have an embedding $S_n \hookrightarrow \operatorname{Gal}(L/F)$, showing that $|\operatorname{Gal}(L/F)| \ge |S_n| = n!$.[/guided]

[step:Apply Artin's Lemma to show $F = L^{S_n}$ and force $|\operatorname{Gal}(L/F)| = n!$]Via the injection $\varphi$, we identify $S_n$ with a subgroup of $\operatorname{Aut}(L)$. We apply [Artin's Lemma](/theorems/1272). The hypotheses of Artin's Lemma require: 1. $L$ is a field. This holds: $L = K(x_1, \ldots, x_n)$ is a rational function field. 2. $S_n$ (identified with its image under $\varphi$) is a finite subgroup of $\operatorname{Aut}(L)$. This holds: $\varphi$ is an injective group homomorphism from the finite group $S_n$ to $\operatorname{Aut}(L)$. [Artin's Lemma](/theorems/1272) concludes that $L/L^{S_n}$ is a finite Galois extension with $\operatorname{Gal}(L/L^{S_n}) = S_n$ (under the identification via $\varphi$) and $[L : L^{S_n}] = |S_n| = n!$. We established in the third step that every $\varphi_\sigma$ fixes $F$ pointwise, so $F \subset L^{S_n}$. We now show $F = L^{S_n}$ by a degree comparison. Since $f(t) = \prod_{i=1}^n(t - x_i) \in F[t]$ has degree $n$ and $x_1$ is a root of $f$, the extension $F(x_1)/F$ has degree $[F(x_1) : F] \le n$ (the minimal polynomial of $x_1$ over $F$ divides $f$). Over $F(x_1)$, the polynomial $f(t)/(t - x_1)$ has degree $n - 1$ and $x_2$ is a root, so $[F(x_1, x_2) : F(x_1)] \le n - 1$. Continuing inductively, $[F(x_1, \ldots, x_k) : F(x_1, \ldots, x_{k-1})] \le n - k + 1$ for each $k = 1, \ldots, n$. By the [Tower Law](/theorems/1248), \begin{align*} [L : F] &= [F(x_1, \ldots, x_n) : F] \\ &= \prod_{k=1}^n [F(x_1, \ldots, x_k) : F(x_1, \ldots, x_{k-1})] \\ &\le n \cdot (n-1) \cdot (n-2) \cdots 1 = n!. \end{align*} Now, since $F \subset L^{S_n} \subset L$, multiplicativity of degrees gives \begin{align*} [L : F] = [L : L^{S_n}] \cdot [L^{S_n} : F] = n! \cdot [L^{S_n} : F]. \end{align*} From $[L : F] \le n!$ we obtain $n! \cdot [L^{S_n} : F] \le n!$, which forces $[L^{S_n} : F] = 1$, i.e., $L^{S_n} = F$. Therefore $[L : F] = n!$ and $\operatorname{Gal}(L/F) = \operatorname{Gal}(L/L^{S_n}) = S_n$ (under the identification $\varphi$). This completes the proof that $L/F$ is Galois with $\operatorname{Gal}(L/F) \cong S_n$.[/step]

[guided]The injection $S_n \hookrightarrow \operatorname{Gal}(L/F)$ from the previous step tells us that $|\operatorname{Gal}(L/F)| \ge n!$. To show equality, we need the reverse inequality. The strategy uses Artin's Lemma to pin down the fixed field and then compares degrees. **Applying Artin's Lemma.** We verify the hypotheses of [Artin's Lemma](/theorems/1272): - $L = K(x_1, \ldots, x_n)$ is a field. - The image $\varphi(S_n) \subset \operatorname{Aut}(L)$ is a finite group of order $n!$. Artin's Lemma concludes: $L / L^{S_n}$ is a finite Galois extension with $[L : L^{S_n}] = |S_n| = n!$ and $\operatorname{Gal}(L/L^{S_n}) = \varphi(S_n) \cong S_n$. **Locating $F$ relative to $L^{S_n}$.** We showed that every $\varphi_\sigma$ fixes $F$ pointwise. By definition, $L^{S_n} = \{a \in L : \varphi_\sigma(a) = a \text{ for all } \sigma \in S_n\}$. Since each element of $F$ is fixed by every $\varphi_\sigma$, we have $F \subset L^{S_n}$. Could the inclusion be strict? **Bounding $[L : F]$ from above.** We use the tower $F \subset F(x_1) \subset F(x_1, x_2) \subset \cdots \subset F(x_1, \ldots, x_n) = L$. At the $k$-th stage, $x_k$ is a root of the polynomial \begin{align*} g_k(t) := \prod_{\substack{i=1 \\ i \ne i_1, \ldots, i \ne i_{k-1}}}^n (t - x_i) = \frac{f(t)}{\prod_{j=1}^{k-1}(t - x_j)} \in F(x_1, \ldots, x_{k-1})[t], \end{align*} which has degree $n - k + 1$. The minimal polynomial of $x_k$ over $F(x_1, \ldots, x_{k-1})$ divides $g_k$, so $[F(x_1, \ldots, x_k) : F(x_1, \ldots, x_{k-1})] \le n - k + 1$. By the [Tower Law](/theorems/1248) applied iteratively, \begin{align*} [L : F] = \prod_{k=1}^n [F(x_1, \ldots, x_k) : F(x_1, \ldots, x_{k-1})] \le n!. \end{align*} **Forcing equality.** The tower $F \subset L^{S_n} \subset L$ gives $[L : F] = [L : L^{S_n}] \cdot [L^{S_n} : F] = n! \cdot [L^{S_n} : F]$ by the [Tower Law](/theorems/1248). Since $[L : F] \le n!$, we need $[L^{S_n} : F] \le 1$. Since $[L^{S_n} : F] \ge 1$ (as $F \subset L^{S_n}$), we conclude $[L^{S_n} : F] = 1$, i.e., $F = L^{S_n}$. Substituting back: $[L : F] = n!$ and $\operatorname{Gal}(L/F) = \operatorname{Gal}(L/L^{S_n}) = S_n$. This is the heart of the proof. The inclusion $F \subset L^{S_n}$ (which follows from the invariance of the elementary symmetric polynomials) could in principle be strict — the fixed field $L^{S_n}$ might contain rational functions in $x_1, \ldots, x_n$ that are symmetric but not expressible in terms of $u_1, \ldots, u_n$. The degree argument rules this out without ever invoking the Fundamental Theorem of Symmetric Polynomials directly. In fact, the equality $F = L^{S_n}$ is itself a form of the Fundamental Theorem: it states that every symmetric rational function in $x_1, \ldots, x_n$ is a rational function of the elementary symmetric polynomials $u_1, \ldots, u_n$.[/guided]