English
There exists a prime p and n ∈ ℕ⁺ such that CharP K p and card K = p^n, i.e., the field order is a prime power with corresponding prime characteristic.
Русский
Существует простое p и n ∈ ℕ⁺ такие, что CharP K p и card K = p^n, то есть порядок поля — простая степень простого числа.
LaTeX
$$$\exists p \in \mathbb{N},\; p \text{ prime} \land \exists n \in \mathbb{N}_{>0},\; \text{CharP } K\ p \land |K| = p^{n}$$$
Lean4
/-- The cardinality `q` is a power of the characteristic of `K`. -/
@[stacks 09HY "first part"]
theorem card (p : ℕ) [CharP K p] : ∃ n : ℕ+, Nat.Prime p ∧ q = p ^ (n : ℕ) :=
by
haveI hp : Fact p.Prime := ⟨CharP.char_is_prime K p⟩
letI : Module (ZMod p) K := { (ZMod.castHom dvd_rfl K : ZMod p →+* _).toModule with }
obtain ⟨n, h⟩ := VectorSpace.card_fintype (ZMod p) K
rw [ZMod.card] at h
refine ⟨⟨n, ?_⟩, hp.1, h⟩
apply Or.resolve_left (Nat.eq_zero_or_pos n)
rintro rfl
rw [pow_zero] at h
have : (0 : K) = 1 := by apply Fintype.card_le_one_iff.mp (le_of_eq h)
exact absurd this zero_ne_one
