Prime fields

A prime field is a field that does not contain any nontrivial subfield. Prime fields are ℚ in characteristic 0 and ZMod p in characteristic p with p a prime number. Any field K contains a unique prime field: it is the smallest field contained in K.

Results

• The fields ℚ and ZMod p are prime fields. These are stated as the instances that says that the corresponding Subfield type is a Subsingleton.
• Subfield.bot_eq_of_charZero : the smallest subfield of a field of characteristic 0 is (the image of) ℚ.
• Subfield.bot_eq_of_zMod_algebra: the smallest subfield of a field of characteristic p is (the image of) ZMod p.

instance instSubsingletonSubfieldRat : Subsingleton (Subfield ℚ)

instance instSubsingletonSubfieldZMod (p : ℕ) [hp : Fact (Nat.Prime p)] : Subsingleton (Subfield (ZMod p))

theorem Subfield.bot_eq_of_charZero {K : Type u_1} [Field K] [CharZero K] : ⊥ = (algebraMap ℚ K).fieldRange

The smallest subfield of a field of characteristic 0 is (the image of) ℚ.

noncomputable def Subfield.botEquivRat (K : Type u_1) [Field K] [CharZero K] : ↥⊥ ≃+* ℚ

Equivalence between the smallest subfield of a field of characteristic 0 and ℚ.

Equations

• Subfield.botEquivRat K = (RingEquiv.subfieldCongr ⋯).trans (algebraMap ℚ K).rangeRestrictFieldEquiv.symm

theorem Subfield.bot_eq_of_zmod_algebra {K : Type u_1} [Field K] (p : ℕ) [Fact (Nat.Prime p)] [Algebra (ZMod p) K] : ⊥ = (algebraMap (ZMod p) K).fieldRange

The smallest subfield of a field of characteristic p is (the image of) ZMod p. Note that the fact that the field K is of characteristic p is stated by the fact that it is ZMod p-algebra.

@[deprecated Subfield.bot_eq_of_zmod_algebra (since := "2026-10-03")]

theorem Subfield.bot_eq_of_zMod_algebra {K : Type u_1} [Field K] (p : ℕ) [Fact (Nat.Prime p)] [Algebra (ZMod p) K] : ⊥ = (algebraMap (ZMod p) K).fieldRange

Alias of Subfield.bot_eq_of_zmod_algebra.

---

The smallest subfield of a field of characteristic p is (the image of) ZMod p. Note that the fact that the field K is of characteristic p is stated by the fact that it is ZMod p-algebra.

noncomputable def Subfield.botEquivZMod (K : Type u_1) [Field K] (p : ℕ) [Fact (Nat.Prime p)] [Algebra (ZMod p) K] : ↥⊥ ≃+* ZMod p

Equivalence between the smallest subfield of a field of characteristic p and ZMod p.

Equations

• Subfield.botEquivZMod K p = (RingEquiv.subfieldCongr ⋯).trans (algebraMap (ZMod p) K).rangeRestrictFieldEquiv.symm

@[simp]

theorem Subfield.botEquivZMod_symm_apply {K : Type u_1} [Field K] (p : ℕ) [Fact (Nat.Prime p)] [Algebra (ZMod p) K] [Algebra (ZMod p) ↥⊥] (x : ZMod p) : (botEquivZMod K p).symm x = (algebraMap (ZMod p) ↥⊥) x

theorem Subfield.coe_botEquivZMod_symm_apply {K : Type u_1} [Field K] (p : ℕ) [Fact (Nat.Prime p)] [Algebra (ZMod p) K] (x : ZMod p) : ↑((botEquivZMod K p).symm x) = (algebraMap (ZMod p) K) x