Definition df-finfld

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)

	Ref	Expression
Assertion	df-finfld	Could not format assertion : No typesetting found for |- finFld = ( q e. ( ^ " ( Prime X. NN ) ) |-> inf ( ( HFStruct i^i { k e. Field | ( # ` ( Base ` k ) ) = q } ) , HFStruct ,

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfinfld	Could not format finFld : No typesetting found for class finFld with typecode class
1		vq	$$setvarq$$
2		cexp	$$class^$$
3		cprime	$$class\mathbb{P}$$
4		cn	$$class\mathbb{N}$$
5	3 4	cxp	$$class\left(\mathbb{P}\times \mathbb{N}\right)$$
6	2 5	cima	$$class^\left[\mathbb{P}\times \mathbb{N}\right]$$
7		chfstruct	Could not format HFStruct : No typesetting found for class HFStruct with typecode class
8		vk	$$setvark$$
9		cfield	$$class\mathrm{Field}$$
10		chash	$$class\left|.\right|$$
11		cbs	$$class\mathrm{Base}$$
12	8	cv	$$setvark$$
13	12 11	cfv	$$class{\mathrm{Base}}_k$$
14	13 10	cfv	$$class\left|{\mathrm{Base}}_k\right|$$
15	1	cv	$$setvarq$$
16	14 15	wceq	$$wff\left|{\mathrm{Base}}_k\right|=q$$
17	16 8 9	crab	$$class\left\{k\in \mathrm{Field}|\left|{\mathrm{Base}}_k\right|=q\right\}$$
18	7 17	cin	Could not format ( HFStruct i^i { k e. Field | ( # ` ( Base ` k ) ) = q } ) : No typesetting found for class ( HFStruct i^i { k e. Field | ( # ` ( Base ` k ) ) = q } ) with typecode class
19		clthfstruct	Could not format
20	18 7 19	cinf	Could not format inf ( ( HFStruct i^i { k e. Field | ( # ` ( Base ` k ) ) = q } ) , HFStruct ,
21	1 6 20	cmpt	Could not format ( q e. ( ^ " ( Prime X. NN ) ) |-> inf ( ( HFStruct i^i { k e. Field | ( # ` ( Base ` k ) ) = q } ) , HFStruct , inf ( ( HFStruct i^i { k e. Field | ( # ` ( Base ` k ) ) = q } ) , HFStruct ,
22	0 21	wceq	Could not format finFld = ( q e. ( ^ " ( Prime X. NN ) ) |-> inf ( ( HFStruct i^i { k e. Field | ( # ` ( Base ` k ) ) = q } ) , HFStruct , inf ( ( HFStruct i^i { k e. Field | ( # ` ( Base ` k ) ) = q } ) , HFStruct ,