Free $k[x_1, \dots, x_n]^{S_n}$-module? Let $\text{char}\,k = 0$ and $n \ge 2$. What is the easiest way to see that $k[x_1, \dots, x_n]$ is a free $k[x_1, \dots, x_n]^{S_n}$-module with basis$$x_2^{m_2}x_3^{m_3} \dots x_{n-1}^{m_{n-1}} x_n^{m_n},\text{ }m_2 \in [0, 1],\text{ }m_3 \in [0, 2], \dots,\text{ }m_n \in [0, n-1]?$$
 A: It is enough to show that the given generators span $k[x_1, \ldots, x_n]$ as a $k[x_1, \ldots, x_n]^{S_n}$ module. Once we've shown this, it is easy to see that $k(x_1, \ldots, x_n)$ is dimension $n!$ as a $k(x_1, \ldots, x_n)^{S_n}$ vector space, so $n!$ vector which span must be linearly independent.
Notation: For every $r \in \left\{0,1,\ldots,n\right\}$, let $e^r_k$ be the $k$-th elementary symmetric polynomial in $x_1$, ..., $x_r$. Let $R = k[x_1, \ldots, x_n]$ and let $A = R^{S_n}$.
Lemma 1 The polynomial $e^r_k$ is in the ring $A[x_{r+1}, \ldots, x_n]$. 
Proof Induction on $n-r$. The base case, $r=n$, is that $e_k(x_1, \ldots, x_n) \in A$; this is true. Now, $e_k^r = e_k^{r+1} - x_{r+1} e_{k-1}^{r
+1}$, so the result follows by induction. $\square$.
Lemma 2 The monomial $x_r^r$ is in the $A[x_{r+1}, \ldots, x_n]$-linear span of monomials of the form $x_r^s$ with $0 \leq s < r$.
Proof Expand $(x_r-x_1) (x_r-x_2) \cdots (x_r-x_r) = 0$ to get $x_r^r - e^r_1 x_r^{r-1} + e^r_2 x_r^{r-2} - \cdots = 0$ or, in other words, $x_r^r = \sum_{s=0}^{r-1} (-1)^{r-s+1} x_r^s e^r_{r-s}$. Now apply Lemma 1. $\square$
We now prove the following result by induction on $r$: 

The ring $R$ is spanned as an $A[x_{r+1}, \ldots, x_n]$-module by monomials of the form $x_1^{d_1} x_2^{d_2} \cdots x_r^{d_r}$ with $0 \leq d_j < j$.

The base case $r=0$ is trivial (it says $R = A \cdot 1$); the case $r=n$ is the claim.
We now do the inductive step. Since $R$ is spanned as an $A[x_{r}, \ldots, x_n]$-module by monomials of the form $x_1^{d_1} x_2^{d_2} \cdots x_{r-1}^{d_{r-1}}$ with $0 \leq d_j < j$, we know that $R$ is spanned as an $A[x_{r+1}, \ldots, x_n]$-module by monomials of the form $x_1^{d_1} x_2^{d_2} \cdots x_{r-1}^{d_{r-1}} x_r^t$, with $0 \leq d_j < j$, and no bound on $t$. But Lemma 2 allows us to replace $x_r^t$ by lower powers of $x_r$ if $t \geq r$. QED
