English
There is a field structure on α iff |α| is a prime power.
Русский
Существует поле над α тогда, когда мощность α равна простому числу в степени.
LaTeX
$$$\\exists Field\\;\\alpha \\iff |\\alpha| = p^n$ for some prime p and n ≥ 1.$$
Lean4
/-- There is a field structure on type if and only if its cardinality is a prime power. -/
theorem nonempty_iff {α : Type u} : Nonempty (Field α) ↔ IsPrimePow #α :=
by
rw [Cardinal.isPrimePow_iff]
obtain h | h := fintypeOrInfinite α
·
simpa only [Cardinal.mk_fintype, Nat.cast_inj, exists_eq_left', (Cardinal.nat_lt_aleph0 _).not_ge, false_or] using
Fintype.nonempty_field_iff
· simpa only [← Cardinal.infinite_iff, h, true_or, iff_true] using Infinite.nonempty_field
