(a) If \(f \in \mathcal{P}\), then the definition of \(\operatorname {id}_{[N]} \cdot f\) yields

This proves part (a).

(b) Let \(\sigma , \tau \in S_N\) and \(f \in \mathcal{P}\). The definition of \(\sigma \cdot (\tau \cdot f)\) yields

Write the polynomial \(f\) in the form

The definition of \(\tau \cdot f\) yields

Substituting \(x_{\sigma (1)}, x_{\sigma (2)}, \ldots , x_{\sigma (N)}\) for \(x_1, x_2, \ldots , x_N\) on both sides, we obtain

Comparing with 1, we obtain \((\sigma \tau ) \cdot f = \sigma \cdot (\tau \cdot f)\).

Fix \(\sigma \in S_N\). For any \(f, g \in \mathcal{P}\), we have

(by expanding the substitution definition of the action). Thus, the map \(f \mapsto \sigma \cdot f\) respects multiplication. Similarly, this map respects addition, respects scaling, respects the zero and respects the unity. Hence, this map is a \(K\)-algebra morphism from \(\mathcal{P}\) to \(\mathcal{P}\). Furthermore, this map is invertible, since its inverse is the map \(f \mapsto \sigma ^{-1} \cdot f\). Thus, this map is a \(K\)-algebra automorphism of \(\mathcal{P}\).

We need to show that \(\mathcal{S}\) is closed under addition, multiplication and scaling, and that \(\mathcal{S}\) contains the zero and the unity of \(\mathcal{P}\). Let us show that \(\mathcal{S}\) is closed under multiplication (since all the other claims are equally easy): Let \(f, g \in \mathcal{S}\). We must show that \(fg \in \mathcal{S}\).

The polynomial \(f\) is symmetric (since \(f \in \mathcal{S}\)); in other words, \(\sigma \cdot f = f\) for each \(\sigma \in S_N\). Similarly, \(\sigma \cdot g = g\) for each \(\sigma \in S_N\). Now, from 3, we see that for each \(\sigma \in S_N\), we have \(\sigma \cdot (fg) = (\sigma \cdot f) \cdot (\sigma \cdot g) = fg\). This shows that \(fg\) is symmetric, i.e., \(fg \in \mathcal{S}\). The other claims are proved similarly.

Let \(n {\gt} N\) be an integer. Then, the set \([N]\) has no \(n\) distinct elements. Thus, there exists no \(n\)-tuple \((i_1, i_2, \ldots , i_n) \in [N]^n\) satisfying \(i_1 {\lt} i_2 {\lt} \cdots {\lt} i_n\). Now, the definition of \(e_n\) yields

(a) For each \(i \in \{ 1, 2, \ldots , N\} \), we have \(1 + t x_i = \sum _{a \in \{ 0,1\} } (t x_i)^a\). Multiplying these equalities over all \(i \in \{ 1, 2, \ldots , N\} \), we obtain

Substituting \(-t\) for \(t\) gives the stated identity.

(b) This is similar to part (a), using two variables \(u\) and \(v\).

(c) For each \(i \in \{ 1, 2, \ldots , N\} \), we have \(\frac{1}{1 - t x_i} = \sum _{a \in \mathbb {N}} (t x_i)^a\). Multiplying these equalities over all \(i \in \{ 1, 2, \ldots , N\} \), we obtain

The identity \((1 - t x_i) \cdot \sum _{k \geq 0} (t x_i)^k = 1\) is proved by extracting coefficients: the coefficient of \(t^n\) on the left is \(x_i^n - x_i \cdot x_i^{n-1} = 0\) for \(n {\gt} 0\) and \(1\) for \(n = 0\). The product identity follows from \(\prod _i (1 - t x_i) \cdot \prod _i \sum _k (t x_i)^k = \prod _i 1 = 1\).

We prove formulas 7 and 9; the formula 8 can be derived by differentiating the generating function \(\prod _{i=1}^N (1 - t x_i) = \sum _n (-1)^n t^n e_n\) with respect to \(t\), and comparing coefficients (see the source for details).

Proof of 7: In the FPS ring \(\mathcal{P}[[t]]\), by Proposition 6.10 (a) and (c) we have

and

Multiplying these two equalities, the left-hand side becomes

The right-hand side product is \(\sum _{n \in \mathbb {N}} \left(\sum _{j=0}^n (-1)^j e_j h_{n-j}\right) t^n\). Comparing coefficients of \(t^n\) for \(n {\gt} 0\), we obtain 7.

Proof of 9: The proof is by a counting argument on monomials. Each monomial in \(h_n\) corresponds to a multiset \(s\) of size \(n\) from \([N]\). On the left-hand side, each such monomial appears exactly \(n\) times: once for each way to pick an element \(i\) in the support of \(s\) and a positive integer \(j \leq \text{count}(i, s)\), contributing to the term \(h_{n-j} p_j\). For each \(s\), the total count is \(\sum _{i=1}^N \text{count}(i, s) = n\), matching the right-hand side.

Various proofs can be found in [ Benede25 , Theorem 171 ] , [ BluCos16 , proof of Theorem 1 ] , [ Dumas08 , Theorem 1.2.1 ] , [ Goodma15 , Theorem 9.6.6 ] , [ Smith95 , § 1.1 ] .

Part (a): Part (a) is proved by constructing the evaluation map \(K[y_1, \ldots , y_N] \to \mathcal{S}\) sending \(y_k \mapsto e_k\) and showing it is a \(K\)-algebra isomorphism. Algebraic independence follows from injectivity; generation follows from surjectivity.

Part (b): The proof uses the Newton–Girard relations to show that each \(e_k\) (for \(k \leq N\)) can be expressed as a polynomial in \(h_1, \ldots , h_N\), by strong induction on \(k\). The key identity is: from 7, \((-1)^{k+1} e_{k+1} = -\sum _{j=0}^{k} (-1)^j e_j h_{k+1-j}\), where by the induction hypothesis \(e_0, \ldots , e_k\) are already in the range of the evaluation map at \(h_1, \ldots , h_N\). The algebraic independence of the \(h_i\) then follows by a transcendence degree argument: the composition \(K[y_1, \ldots , y_N] \to \mathcal{S} \xrightarrow {\sim } K[y_1, \ldots , y_N]\) (via the isomorphism from part (a)) is a surjective endomorphism, hence bijective since polynomial rings over integral domains have finite transcendence degree.

Note: The Lean proof of part (b) requires the additional hypothesis that \(K\) is an integral domain.

Part (c): The argument is analogous to part (b). Newton’s identity 8 gives \(n \cdot e_n = \sum _{j=1}^n (-1)^{j-1} e_{n-j} p_j\). Since \(K\) is a \(\mathbb {Q}\)-algebra, \(n\) is invertible in \(K\), so we can solve for \(e_n\) as a polynomial in \(e_0, \ldots , e_{n-1}\) and \(p_1, \ldots , p_n\). By strong induction, each \(e_k\) lies in the range of the evaluation map at \(p_1, \ldots , p_N\). Algebraic independence again follows by the transcendence degree argument.

Note: The Lean formalization of part (c) contains sorry in some helper lemmas (weight constraint and triangular structure arguments).

The proof proceeds by showing that invariance under simple transpositions implies invariance under all transpositions of the form \(\text{swap}(i, j)\) for any \(i, j \in [N]\).

Step 1: Invariance under adjacent transpositions implies invariance under arbitrary transpositions. We prove by induction on \(|j - i|\) that \(\text{swap}(i, j) \cdot f = f\). The base case \(|j - i| = 1\) is the hypothesis 10. For the inductive step, use the conjugation identity: \(\text{swap}(i, j) = \text{swap}(i, i+1) \cdot \text{swap}(i+1, j) \cdot \text{swap}(i, i+1)\).

Step 2: Every permutation \(\sigma \in S_N\) can be written as a product of transpositions (this is a standard fact about the symmetric group). Since each transposition fixes \(f\), so does \(\sigma \).

If \(\mathfrak {m} = x_1^{a_1} \cdots x_N^{a_N}\) is squarefree, then each \(a_i \leq 1\), so \(\deg \mathfrak {m} = a_1 + \cdots + a_N \leq N\).

This is the standard identity that the sum of all multiplicities in a multiset equals its cardinality. The proof splits the sum over elements that appear in \(s\) and elements that do not, the latter contributing zero.

For \(e_n\): permuting the variables permutes the strictly increasing \(n\)-tuples \((i_1 {\lt} \cdots {\lt} i_n)\), so the sum is unchanged. For \(h_n\) and \(p_n\): the argument is analogous, using the fact that permuting variables permutes the non-decreasing tuples (for \(h_n\)) or the individual terms \(x_i^n\) (for \(p_n\)).

If \(\mathfrak {m}\) is primal, its support has at most one element. If the support is empty, then \(\mathfrak {m} = 1\). If the support is \(\{ i\} \), then \(\mathfrak {m} = x_i^{m_i}\) for some \(m_i {\gt} 0\). The converse is immediate.

Direct from the definition of monomials in a multivariable polynomial ring.

The monomial \(\mathfrak {m}_S\) is defined as \(\sum _{i \in S} e_i\) where \(e_i\) is the \(i\)-th standard basis vector. Each entry is \(0\) or \(1\) (squarefree), the sum of entries equals \(|S|\) (degree), and the support is exactly \(S\). All properties are proved by induction on \(|S|\).

The degree is defined as the sum of all exponents. Since the exponent vector of \(\mathfrak {m}_1 \cdot \mathfrak {m}_2\) is the pointwise sum of the exponent vectors, the degree of the product equals the sum of the degrees.

These follow directly from the definitions. For \(e_0\) and \(h_0\), the only \(0\)-tuple is the empty tuple, giving an empty product equal to \(1\). For \(e_1\) and \(h_1\), the \(1\)-tuples are the singletons \((i)\) for \(i \in [N]\), giving \(\sum _{i=1}^N x_i\). For \(p_1\), this is \(\sum _{i=1}^N x_i^1 = \sum _{i=1}^N x_i\). For \(p_0\), the Lean definition follows Mathlib’s convention, which gives \(p_0 = \sum _{i=1}^N x_i^0 = N\).

Both follow immediately from the definitions: \(e_n\) is the sum over strictly increasing \(n\)-tuples, which bijects with \(n\)-element subsets \(S \subseteq [N]\); and \(p_n = \sum _{i=1}^N x_i^n\) is the definition for \(n {\gt} 0\).

By case analysis on the sign of \(n\). For non-negative \(n\), symmetry follows from Lemma 6.17. For negative \(n\), the polynomial is \(0\) which is trivially symmetric.

Partition \(\binom {[N+1]}{n+1}\) into subsets not containing \(N+1\) and subsets containing \(N+1\). The first group yields \(e_{n+1}(x_1, \ldots , x_N)\) (via a bijection with \(\binom {[N]}{n+1}\)). The second group yields \(y \cdot e_n(x_1, \ldots , x_N)\) (via a bijection with \(\binom {[N]}{n}\), factoring out the variable \(x_{N+1} = y\)). The proof establishes these bijections explicitly.

For each property, apply a permutation \(\sigma \) and use the linearity of the action. For instance, \(\sigma \cdot (f + g) = \sigma \cdot f + \sigma \cdot g = \operatorname {sign}(\sigma )(f + g)\).

If \(f\) is antisymmetric, then \(\sigma \cdot (f^2) = (\sigma \cdot f)^2 = (\operatorname {sign}(\sigma ) \cdot f)^2 = \operatorname {sign}(\sigma )^2 \cdot f^2 = f^2\), using \(\operatorname {sign}(\sigma )^2 = 1\).

This equals \(e_1\), which is symmetric by Lemma 6.17.