English
If f is a continuous ring homomorphism, then f commutes with the exponential map on elements within the radius of convergence: f(exp(x)) = exp(f(x)).
Русский
Пусть f — непрерывное кольцевое гомоморфное отображение; тогда сопряжение экспоненты с f выполняется для элементов внутри радиуса сходимости: f(exp(x)) = exp(f(x)).
LaTeX
$$$ f(\exp 𝕂 x) = \exp 𝕂 (f x) \quad\text{for } x \in B(0, \operatorname{radius}(\expSeries 𝕂 𝔸))$$$
Lean4
/-- Any continuous ring homomorphism commutes with `NormedSpace.exp`. -/
theorem map_exp_of_mem_ball {F} [FunLike F 𝔸 𝔹] [RingHomClass F 𝔸 𝔹] (f : F) (hf : Continuous f) (x : 𝔸)
(hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : f (exp 𝕂 x) = exp 𝕂 (f x) :=
by
rw [exp_eq_tsum, exp_eq_tsum]
refine ((expSeries_summable_of_mem_ball' _ hx).hasSum.map f hf).tsum_eq.symm.trans ?_
dsimp only [Function.comp_def]
simp_rw [map_inv_natCast_smul f 𝕂 𝕂, map_pow]
