TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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 every prime $p$ and $n \geq 1$ , a field with $p^{n}$ elements exists

Statement

For every prime $p$ and every integer $n \geq 1$ , there exists a field with exactly $p^{n}$ elements.

Facts & Assumptions

Given: A prime $p$ , a positive integer $n$ , and $q = p^{n}$ .

[L1]

In characteristic $p$ , the roots of $t^{q} - t$ in a field form a subfield and are all simple (In characteristic $p$ , the roots of $x^{p^{n}} - x$ form a subfield and are all simple).

[L2]

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

[L3]

The quotient $Z / p$ is a field (For every prime $p$ , the two operations on $Z / p$ make it a field).

[L4]

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

[L5]

A field with finite underlying set is a finite field and its order is its cardinality (Finite fields and their order).

Proof

technique · constructive

1.1

Over the field $F_{p}$ from [L3], use [L2] to choose a splitting field $E$ of $h (t) = t^{q} - t$ .

givenL2L3chooseconstruct

2.1

Let $R$ be the root set of $h$ in $E$ . By [L1], $R$ is a subfield of $E$ and all roots are simple. By [L4], the roots generate $E$ , while the subfield $R$ already contains them and the base; hence $E = R$ .

step 1.1L1L4

3.1

The degree- $q$ polynomial $h$ splits in $E$ and has no repeated roots, so it has exactly $q$ distinct roots. Thus $∣ E ∣ = ∣ R ∣ = q = p^{n}$ .

step 2.1L1algebra

4.1

By [L5], $E$ is the required finite field.

step 3.1L5discharge-construct∎

Depends on

Used by

For every finite field F_q and every n≥1, a monic irreducible polynomial of degree n exists Corollary
FALSE: degrees add in a tower of finite field extensions False statement
FALSE: F_pⁿ is the ring ℤ/pⁿℤ False statement
Over F_q, x^qⁿ-x is the product of all monic irreducibles whose degrees divide n Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 80 results over 14 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, Finite Fields, Theorem 2.5 (standard reference, not scraped)
J. S. Milne, Fields and Galois Theory, Propositions 4.19-4.24 (standard reference, not scraped)

For every prime pp and n≥1n≥1, a field with pnpn elements exists