ringHom_eq_id_or_conj_of_continuous

English

The only continuous ring homomorphisms f: ℂ → ℂ are the identity and complex conjugation.

Русский

Единственные непрерывные кольцевые гомоморфизмы f: ℂ → ℂ — тождественный отображение и сопряжение.

LaTeX

$$$ f = \\mathrm{id}_{\\\\mathbb{C}} \\\\lor f = \\\\mathrm{conj}$$$

Lean4

/-- The only continuous ring homomorphisms from `ℂ` to `ℂ` are the identity and the complex
conjugation. -/
theorem ringHom_eq_id_or_conj_of_continuous {f : ℂ →+* ℂ} (hf : Continuous f) : f = RingHom.id ℂ ∨ f = conj := by
  simpa only [DFunLike.ext_iff] using real_algHom_eq_id_or_conj (AlgHom.mk' f (map_real_smul f hf))

Похожие утверждения