mathlib3 documentation


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.

A fintype can be given a field structure iff its cardinality is a prime power.

theorem infinite.nonempty_field {α : Type u} [infinite α] :

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.