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 field with elements is the splitting field of over its prime subfield
Statement
If is a field with elements, then every satisfies , and is the splitting field of over its prime subfield.
Facts & Assumptions
Given: A finite field of order .
The group is cyclic (The multiplicative group of a finite field is cyclic).
A splitting field is generated over the base by all roots of the polynomial (Polynomials that split and splitting fields of a polynomial or a family of polynomials).
A nonzero degree- polynomial over a domain has at most distinct roots (A nonzero polynomial of degree over an integral domain has at most distinct roots).
Proof
The cyclic group has order , so every nonzero satisfies and hence . The equality also holds for .
Thus all elements of are roots of . By [L4] there are no other distinct roots in any extension, so the polynomial splits into its linear factors over .
The set of roots is all of , so it generates over its prime subfield. By [L3], is the splitting field.
Depends on
Used by
- The relative Frobenius x↦ x^q of an extension of finite fields Definition
- Fₚ is the union of its finite subfields and is an infinite algebraic extension Example
- For a degree-n extension of a field of order q, the q-power map has order exactly n Lemma
- If p is a prime not dividing n, a rational minimal polynomial of a primitive n-th root of unity also kills its p-th power Lemma
- The elements of a finite extension fixed by the q-power map are exactly the base field Lemma
- A monic irreducible of degree d over F_q has the d distinct roots α,α^q,…,α^qᵈ⁻¹ Theorem
- Finite fields of the same order are isomorphic Theorem
- Over F_q, x^qⁿ-x is the product of all monic irreducibles whose degrees divide n Theorem
- The subfields of F_pⁿ are the unique fields F_pᵈ for positive divisors d of n Theorem
Dependency tree · two levels
13 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
- K. Conrad, Finite Fields, Section 2 (standard reference, not scraped)