CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A symmetric polynomial in the roots of a monic polynomial is a polynomial in its coefficients and lies in the base ring

Statement

Let $f (t) = t^{n} + a_{1} t^{n - 1} + \dots + a_{n} \in R [t]$ be monic and split in a commutative $R$ -algebra with roots $α_{1}, \dots, α_{n}$ . For every symmetric $P \in R [x_{1}, \dots, x_{n}]$ there is a unique $Q \in R [T_{1}, \dots, T_{n}]$ with

$P = Q (e_{1}, \dots, e_{n}) in R [x_{1}, \dots, x_{n}],$

and for that $Q$ ,

$P (α_{1}, \dots, α_{n}) = Q (- a_{1}, a_{2}, \dots, (- 1)^{n} a_{n}) .$

In particular this value lies in the image of $R$ and is independent of the ordering of the roots. The uniqueness asserted is uniqueness of the representing identity $P = Q (e_{1}, \dots, e_{n})$ , not uniqueness of a $Q$ satisfying the displayed evaluated equality: when $n \geq 1$ and $R$ is not the zero ring, $T_{1} + a_{1}$ is a nonzero polynomial vanishing at $(- a_{1}, a_{2}, \dots, (- 1)^{n} a_{n})$ , so $Q + (T_{1} + a_{1})$ has the same value there as $Q$ .

Facts & Assumptions

Given: A split monic polynomial $f$ and a symmetric polynomial $P$ as in the Statement.

[L1]

Every symmetric polynomial has a unique expression $P = Q (e_{1}, \dots, e_{n})$ (Fundamental theorem of symmetric polynomials: unique expression as a polynomial in $e_{1}, \dots, e_{n}$ ).

[L2]

For the roots of a split monic polynomial, $e_{k} (α_{1}, \dots, α_{n}) = (- 1)^{k} a_{k}$ (Vieta's formulas identify the coefficients of a split monic polynomial with elementary symmetric functions of its roots).

Proof

technique · direct

1.1givenL1

Use [L1] to write $P = Q (e_{1}, \dots, e_{n})$ for a unique $Q$ .

2.1step 1.1L2algebra

Evaluate at the roots and apply [L2] in each coordinate to obtain $P (α_{1}, \dots, α_{n}) = Q (- a_{1}, a_{2}, \dots, (- 1)^{n} a_{n})$ .

3.1step 1.1step 2.1L1∎

The right side is computed from coefficients in $R$ , and symmetry makes it unchanged when the roots are reordered. The asserted uniqueness is the uniqueness in [L1] of the $Q$ representing $P$ as an identity of polynomials, and it is not uniqueness of a $Q$ satisfying the evaluated equality alone: when $n \geq 1$ and $1 \neq 0$ in $R$ , the polynomial $T_{1} + a_{1}$ has $T_{1}$ -coefficient $1$ and is therefore nonzero, while substituting the tuple $(- a_{1}, a_{2}, \dots, (- 1)^{n} a_{n})$ sends it to $- a_{1} + a_{1} = 0$ , so $Q$ and $Q + (T_{1} + a_{1})$ take the same value there.

Depends on

Used by

The discriminant of a monic polynomial as the coefficient expression of Δₙ² Definition
The resolvent cubic of a monic quartic Definition

Dependency tree · two levels

6 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

J. S. Milne, Fields and Galois Theory, Theorem 5.36 and Remark 5.37 (standard reference, not scraped)
K. Conrad, Symmetric Polynomials, Sections 1-2 (standard reference, not scraped)