Some results about the topology of ℂ #

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.