CorollaryStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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.

Every finite family of nonzero polynomials has a splitting field, obtained from their product

Statement

Let $f_{1}, \dots, f_{m} \in F [x]$ be nonzero, where $m \in N$ . A splitting field of the product $h = \prod_{j = 1}^{m} f_{j}$ is a splitting field of the family ${f_{1}, \dots, f_{m}}$ . Hence every finite family of nonzero polynomials has a splitting field. For $m = 0$ , $h = 1$ and the splitting field is $F$ .

Facts & Assumptions

Given: A finite family $f_{1}, \dots, f_{m}$ of nonzero polynomials over a field $F$ .

[F1]

Nonzero polynomial products over a domain are nonzero (Over an integral domain, degrees add under multiplication of nonzero polynomials).

[F2]

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

[F3]

For every field $K$ , the polynomial ring $K [x]$ is a unique factorisation domain (For every field $F$ , $F [x]$ is a unique factorisation domain).

[F4]

A splitting field is generated by all roots of the polynomial or family that splits there (Polynomials that split and splitting fields of a polynomial or a family of polynomials).

Proof

technique · direct

1.1

If $m = 0$ , the product is $1$ , whose empty root set has splitting field $F$ by [F4]. Assume now that $m > 0$ . By [F1], $h$ is nonzero, so [F2] gives a splitting field $E / F$ of $h$ .

F1F2F4

2.1

Each $f_{j}$ divides $h$ in $E [x]$ . Since $h$ is a product of linear factors there, unique factorisation in the ring $E [x]$ from [F3] shows that every irreducible factor of $f_{j}$ is linear; hence every $f_{j}$ splits over $E$ .

F3step 1.1

3.1

An element of an extension is a root of $h = f_{1} \dots f_{m}$ exactly when it is a root of at least one $f_{j}$ , because a field has no zero divisors. Thus the roots generating $E$ are precisely the union of the roots of the family, and [F4] makes $E$ its splitting field.

F4step 1.1algebra∎

Depends on

Used by

The splitting field of {x²-2,x²-3} over ℚ is ℚ(√2,√3) Example

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 40 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

J. S. Milne, Fields and Galois Theory, Chapter 2 (standard reference, not scraped)