Cardinality of Fields

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.

theorem Fintype.isPrimePow_card_of_field {α : Type u_1} [Fintype α] [Field α] : IsPrimePow (Fintype.card α)

A finite field has prime power cardinality.

theorem Fintype.nonempty_field_iff {α : Type u_1} [Fintype α] : Nonempty (Field α) ↔ IsPrimePow (Fintype.card α)

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

theorem Fintype.not_isField_of_card_not_prime_pow {α : Type u_1} [Fintype α] [Ring α] : ¬IsPrimePow (Fintype.card α) → ¬IsField α

theorem Infinite.nonempty_field {α : Type u} [Infinite α] : Nonempty (Field α)

Any infinite type can be endowed a field structure.

theorem Field.nonempty_iff {α : Type u} : Nonempty (Field α) ↔ IsPrimePow (Cardinal.mk α)

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