Cardinality of Fields #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
In this file we show all the possible cardinalities of fields. All infinite cardinals can harbour
a field structure, and so can all types with prime power cardinalities, and this is sharp.
Main statements #
A finite field has prime power cardinality.
fintype can be given a field structure iff its cardinality is a prime power.
Any infinite type can be endowed a field structure.
There is a field structure on type if and only if its cardinality is a prime power.