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 #

fintype.nonempty_field_iff: A fintype can be given a field structure iff its cardinality is a prime power.
infinite.nonempty_field : Any infinite type can be endowed a field structure.
field.nonempty_iff : There is a field structure on type iff its cardinality is a prime power.

source

theorem fintype.is_prime_pow_card_of_field {α : Type u_1} [fintype α] [field α] :

is_prime_pow (fintype.card α)

A finite field has prime power cardinality.

source

theorem fintype.nonempty_field_iff {α : Type u_1} [fintype α] :

nonempty (field α) ↔ is_prime_pow (fintype.card α)

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

source

theorem fintype.not_is_field_of_card_not_prime_pow {α : Type u_1} [fintype α] [ring α] :

¬is_prime_pow (fintype.card α) → ¬is_field α

source

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

nonempty (field α)

Any infinite type can be endowed a field structure.

source

theorem field.nonempty_iff {α : Type u} :

nonempty (field α) ↔ is_prime_pow (cardinal.mk α)

There is a field structure on type if and only if its cardinality is a prime power.