Documentation

Mathlib.Topology.Instances.Complex

Some results about the topology of ℂ #

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.