map_exp — Mathlib

English

Any continuous ring homomorphism f commutes with the exponential map: f(exp x) = exp(f x).

Русский

Любое непрерывное кольцевое гомоморфное отображение сохраняет экспоненту: f(exp x) = exp(f x).

LaTeX

$$$f(\\exp 𝕂 x) = \\exp 𝕂 (f x)$$$

Lean4

/-- Any continuous ring homomorphism commutes with `NormedSpace.exp`. -/
theorem map_exp {F} [FunLike F 𝔸 𝔹] [RingHomClass F 𝔸 𝔹] (f : F) (hf : Continuous f) (x : 𝔸) :
    f (exp 𝕂 x) = exp 𝕂 (f x) :=
  map_exp_of_mem_ball f hf x <| (expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _

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