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) ℚ.

theorem Subfield.bot_eq_of_zMod_algebra {K : Type u_1} (p : ℕ) [hp : Fact (Nat.Prime p)] [Field K] [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.