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 and their order
Definition
A finite field is a field whose underlying set is finite. Its order is its finite cardinality, written .
Once existence and uniqueness are proved, denotes a field of order up to isomorphism. The notation does not assert that the field is the quotient ring .
Depends on
Used by
- The norm of a prime ideal Corollary
- Primes above and residue degree Definition
- Standard subgroups of finite general linear groups Definition
- Sum-check with explicit degree bounds Definition
- The relative Frobenius x↦ x^q of an extension of finite fields Definition
- Affine linear Frobenius groups over finite fields Example
- Gal(F₈/F₂) is cyclic of order three with no proper intermediate field Example
- Grassmannians as maximal parabolic quotients Example
- The intermediate fields of F_2¹²/F₂ match the divisors of twelve Example
- Quadratic forms of dimension at least three over odd finite fields are isotropic Lemma
- The elements of a finite extension fixed by the q-power map are exactly the base field Lemma
- Cardinality of a finite Bruhat cell Proposition
- Every finite field has order pⁿ for a unique prime characteristic p and positive integer n Theorem
- Every finite Galois extension has a normal basis Theorem
- For every prime p and n≥1, a field with pⁿ elements exists Theorem
- For gcd(n,q)=1 the image of Gal(F_q(μₙ)/F_q) in (ℤ/n)^× is generated by [q] Theorem
- The multiplicative group F_q^× of a finite field is cyclic Theorem
Dependency tree · two levels
9 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, Sections 1-2 (standard reference, not scraped)