English
A finite type α can be given a field structure if and only if its cardinality is a prime power.
Русский
Конечный по базису тип может быть полем тогда и только тогда, когда мощность кардинала равна p^n.
LaTeX
$$$\\text{Nonempty Field } \\alpha \\iff \\text{IsPrimePow } |\\alpha|$$$
Lean4
/-- A `Fintype` can be given a field structure iff its cardinality is a prime power. -/
theorem nonempty_field_iff {α} [Fintype α] : Nonempty (Field α) ↔ IsPrimePow ‖α‖ :=
by
refine ⟨fun ⟨h⟩ => Fintype.isPrimePow_card_of_field, ?_⟩
rintro ⟨p, n, hp, hn, hα⟩
haveI := Fact.mk hp.nat_prime
haveI : Fintype (GaloisField p n) := Fintype.ofFinite (GaloisField p n)
exact ⟨(Fintype.equivOfCardEq (((Fintype.card_eq_nat_card).trans (GaloisField.card p n hn.ne')).trans hα)).symm.field⟩
