Some results about the topology of ℂ #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
theorem
complex.subfield_eq_of_closed
{K : subfield ℂ}
(hc : is_closed ↑K) :
K = complex.of_real.field_range ∨ K = ⊤
The only closed subfields of ℂ are ℝ and ℂ.
theorem
complex.uniform_continuous_ring_hom_eq_id_or_conj
(K : subfield ℂ)
{ψ : ↥K →+* ℂ}
(hc : uniform_continuous ⇑ψ) :
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.