Alphabeta MathHow 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 -dimensional vector space over a field with elements has exactly elements
Statement
Let be a finite field with elements, and let be a -dimensional -vector space. Then
Facts & Assumptions
Given: a finite field with elements, and a -dimensional vector space over .
Choosing an ordered basis of length gives a unique coordinate vector in for every element of (A finite list is an ordered basis if and only if every equals for exactly one ; those scalars are the coordinates of in that ordered basis).
The set of functions from a -element set to a -element set has cardinality (The set of functions between finite sets is finite, with , Exponentiation of natural numbers, , and its agreement with the integer power in ).
Proof
By [F1], an ordered basis of identifies bijectively with .
Since has elements, [F2] gives . Transporting cardinality along the bijection of step 1.1 gives .
Remarks
- The boundary case is included: the zero-dimensional vector space has one element and .
Depends on
- Vector space over a field
- Finite-dimensional vector space, and its dimension $\dim_F V$; infinite-dimensional means having no finite basis
- Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis
- A finite list $v : n \to V$ is an ordered basis if and only if every $x \in V$ equals $\sum_{i<n} \lambda_i v_i$ for exactly one $\lambda : n \to F$; those scalars are the coordinates of $x$ in that ordered basis
- The set $A^{B}$ of functions $B \to A$ between finite sets is finite, with $\lvert A^{B}\rvert = \lvert A\rvert^{\lvert B\rvert}$
- Exponentiation of natural numbers, $m^{n}$, and its agreement with the integer power in $\mathbb{R}$
- The cardinality $\lvert A\rvert$ of a finite set
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
- L. Babai and P. Frankl, Linear Algebra Methods in Combinatorics, §2.3.2 (standard reference, not scraped)