Some results about the topology of ℂ

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

The only closed subfields of ℂ are ℝ and ℂ.

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

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.