TheoremStatement: 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.

Vieta expansion: $\prod_{i = 1}^{n} (t - x_{i}) = \sum_{k = 0}^{n} (- 1)^{k} e_{k} t^{n - k}$

Statement

In $R [x_{1}, \dots, x_{n}, t]$ one has

$\prod_{i = 1}^{n} (t - x_{i}) = \sum_{k = 0}^{n} (- 1)^{k} e_{k} (x_{1}, \dots, x_{n}) t^{n - k} .$

For $n = 0$ , both sides are the empty product $1$ .

Facts & Assumptions

Given: A commutative ring $R$ and variables $x_{1}, \dots, x_{n}, t$ .

[L1]

The elementary symmetric polynomial $e_{k}$ is the sum of the products $x_{i_{1}} \dots x_{i_{k}}$ over all $k$ -element subsets of the variables, and $e_{0} = 1$ (The elementary symmetric polynomials $e_{0}, e_{1}, \dots, e_{n}$ ).

[L2]

Natural powers in a monoid satisfy $g^{0} = e$ and $g^{r + 1} = g^{r} g$ (Powers $g^{n}$ : natural exponents in a monoid and integer exponents in a group, with $g^{0} = e$ ).

Proof

technique · direct

1.1

In expanding the product, choose either $t$ or $- x_{i}$ from each factor. A choice of $- x_{i}$ from exactly the indices in a subset $S$ of size $k$ contributes $(- 1)^{k} (\prod_{i \in S} x_{i}) t^{n - k}$ .

givenL2algebra

2.1

Summing the contributions with $∣ S ∣ = k$ gives $(- 1)^{k} e_{k} t^{n - k}$ by the definition of $e_{k}$ .

step 1.1L1

3.1

Summing over $0 \leq k \leq n$ accounts for every term in the expansion exactly once and proves the identity. If $n = 0$ , the sole term is $e_{0} t^{0} = 1$ .

step 2.1L1L2∎

Depends on

Used by

Vieta's formulas identify the coefficients of a split monic polynomial with elementary symmetric functions of its roots Corollary

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 42 results over 13 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

K. Conrad, Symmetric Polynomials, Section 1 (standard reference, not scraped)

Vieta expansion: ∏i=1n(t−xi)=∑k=0n(−1)kektn−k∏i=1n​(t−xi​)=∑k=0n​(−1)kek​tn−k