Theorems · Theorem · general topology

Complex.uniformContinuous_ringHom_eq_id_or_conj

∀ (K : Subfield ℂ) {ψ : ↥K →+* ℂ},
  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.

Defined in

Mathlib.Topology.Instances.Complex

Cited by

1 results in Mathlib

Foundations

Depth 166 from the axioms · uses propext, Classical.choice, Quot.sound