Description: Define a function taking a prime power q to the finite field of
order q . When q is an integer, there is a field of order q
(that is, its base set has q elements) if and only if q is a
prime power. Additionally, any two finite fields of the same order are
isomorphic. Thus, we usually refer to "the" finite field of order q
— which is often denoted 𝔽q
— without specifying a particular one. Usually, this causes no
problems, but in Metamath the notation ( finFldq ) must
unambigously denote a specific set. Since HFStructs can be
well-ordered, we can use the smallest candidate according to the
ordering. This depends on the fact that any finite field is isomorphic
to an HFStruct. Indeed, this isomorphism result holds for most abstract
mathematical structures with a finite base set. (For groups, see
fingrphf .) Thus, the technique used here could apply in other cases
in which we want a particular representative of some class of finite
structures. (Contributed by Eric Schmidt, 24-Oct-2026)