CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.1

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

givenL1

2.1

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})$ .

step 1.1L2algebra

3.1

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.

step 1.1step 2.1L1∎

Depends on

Used by

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

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 15 results over 5 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click 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)