Prime fields

Stream: Is there code for X?

[Xavier Roblot]

Do you have anything about prime fields, in the sense of fields that do not contain any nontrivial subfield? I am mostly interested in something like this:

instance : Subsingleton (Subfield ℚ) := sorry

[Xavier Roblot]

Well, here is what I came up with

import Mathlib.Algebra.Algebra.Rat
import Mathlib.Algebra.Field.Subfield.Basic

instance : Subsingleton (Subfield ℚ) := by
  refine ⟨fun F G ↦ Subfield.ext fun x ↦ ?_⟩
  change (algebraMap ℚ F x).val ∈ _ ↔ (algebraMap ℚ G x).val ∈ _
  simp_rw [SetLike.coe_mem]

theorem Subfield.bot_eq_of_charZero {K : Type*} [Field K] [CharZero K] :
    (⊥ : Subfield K) = (algebraMap ℚ K).fieldRange := by
  rw [eq_comm, eq_bot_iff, ← Subfield.map_bot (algebraMap ℚ K),
    subsingleton_iff_bot_eq_top.mpr inferInstance, ← RingHom.fieldRange_eq_map]

[Kenny Lau]

import Mathlib.Algebra.Field.Subfield.Basic
import Mathlib.Data.Rat.Cast.CharZero

instance : Subsingleton (Subfield ℚ) := subsingleton_of_top_le_bot fun x _ ↦
  have h := Subsingleton.elim ((⊥ : Subfield ℚ).subtype.comp (Rat.castHom _)) (.id _ : ℚ →+* ℚ)
  (congr($h x) : _ = x) ▸ Subtype.prop _

[Xavier Roblot]

#31655