Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

Finite fields of the same order are isomorphic

Statement

Any two finite fields with the same order q are isomorphic. More precisely, after identifying their prime subfields with Fp, there is an isomorphism fixing Fp pointwise. The isomorphism need not be unique.

Facts & Assumptions

Given: Finite fields E and E′ with ∣E∣=∣E′∣=q.

[L1]

Every finite field has prime-power order with base equal to its characteristic prime (Every finite field has order pn for a unique prime characteristic p and positive integer n).

[L2]

A field of order q is a splitting field of tq−t over its prime subfield (A field with q elements is the splitting field of xq−x over its prime subfield).

[L3]

Two splitting fields of the same nonzero polynomial over a base field are isomorphic by an isomorphism fixing the base (Any two splitting fields of a polynomial are isomorphic over the base field).

[L4]

The prime subfield of a characteristic-p field is isomorphic to Fp (A field's prime subfield is isomorphic to Q in characteristic zero and to Fp in characteristic p).

Proof

technique · direct
1.1givenL1L4L5

By [L1], each field has prime-power order with base equal to its characteristic prime. Since the orders are the same, [L5] makes these primes equal, say to p. Use [L4] to identify both prime subfields with one copy of Fp.

2.1step 1.1L2

By [L2], E and E′ are splitting fields of the same polynomial tq−t over this base.

3.1step 2.1L3∎

Apply [L3] to obtain a base-fixing field isomorphism E→E′. Splitting-field uniqueness asserts existence, not uniqueness, so no stronger claim follows.

Depends on

Used by

Dependency tree · two levels

48 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