ringHom_eq_ofReal_of_continuous — Mathlib

English

The only continuous ring homomorphism f: ℝ → ℂ is the inclusion (ofRealHom).

Русский

Единственный непрерывный кольцевой гомоморфизм f: ℝ → ℂ — это включение (ofRealHom).

LaTeX

$$$ f = ofRealHom $$$

Lean4

/-- The only continuous ring homomorphism from `ℝ` to `ℂ` is the identity. -/
theorem ringHom_eq_ofReal_of_continuous {f : ℝ →+* ℂ} (h : Continuous f) : f = ofRealHom := by
  convert congr_arg AlgHom.toRingHom <| Subsingleton.elim (AlgHom.mk' f <| map_real_smul f h) (Algebra.ofId ℝ ℂ)

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