Some results about the topology of ℂ

theorem Complex.subfield_eq_of_closed {K : Subfield ℂ} (hc : IsClosed ↑K) : K = RingHom.fieldRange Complex.ofReal ∨ K = ⊤

The only closed subfields of ℂ are ℝ and ℂ.

theorem Complex.uniformContinuous_ringHom_eq_id_or_conj (K : Subfield ℂ) {ψ : { x // x ∈ K } →+* ℂ} (hc : UniformContinuous ↑ψ) : ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)

Let K a subfield of ℂ and let ψ : K →+* ℂ a ring homomorphism. Assume that ψ is uniform continuous, then ψ is either the inclusion map or the composition of the inclusion map with the complex conjugation.