mathlib3 documentation


Some results about the topology of ℂ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The only closed subfields of are and .

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.