Documentation

Mathlib.Topology.Instances.Complex

Some results about the topology of ℂ #

theorem Complex.subfield_eq_of_closed {K : Subfield } (hc : IsClosed K) :
K = Complex.ofRealHom.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.