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.

For monic $f, g$ of degrees $n, m$ , $Res (f, g) = (- 1)^{m n} Res (g, f)$

Statement

Let $F$ be a field and let $f, g \in F [t]$ be monic of degrees $n, m$ . Then

$Res (f, g) = (- 1)^{m n} Res (g, f) .$

Facts & Assumptions

Given: Monic polynomials $f, g \in F [t]$ of degrees $n, m$ .

[L1]

In a common splitting extension, $Res (f, g) = \prod_{i, j} (α_{i} - β_{j})$ and $Res (g, f) = \prod_{j, i} (β_{j} - α_{i})$ (For monic $f, g$ of degrees $n, m$ splitting in a common extension, $Res (f, g) = \prod_{i = 1}^{n} \prod_{j = 1}^{m} (α_{i} - β_{j})$ ).

[L2]

Every nonzero polynomial over a field has a splitting field (Every nonzero polynomial over a field has a splitting field).

Proof

technique · direct

1.1

Take a splitting field of the nonzero polynomial $f g$ when both degrees are positive; if one polynomial is $1$ , use any splitting field for the other.

givenL2

2.1

Apply [L1] in that field. Replacing each of the $m n$ factors $α_{i} - β_{j}$ by $- (β_{j} - α_{i})$ contributes the factor $(- 1)^{m n}$ and yields the formula.

step 1.1L1algebra

3.1

If $n = 0$ or $m = 0$ , both resultants are $1$ and $(- 1)^{m n} = 1$ , so the same identity holds.

L1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 23 results over 8 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, Proposition 4.35(a) (standard reference, not scraped)

For monic f,gf,g of degrees n,mn,m, Res⁡(f,g)=(−1)mnRes⁡(g,f)Res(f,g)=(−1)mnRes(g,f)