algebraMap_exp_comm_of_mem_ball — Mathlib

English

For x in the ball, the algebra map commutes with the exponential: algebraMap 𝕂 𝔸 (exp 𝕂 x) = exp 𝕂 (algebraMap 𝕂 𝔸 x).

Русский

Для x внутри шара алгебраическая карта совместима с экспонентой: algebraMap 𝕂 𝔸 (exp 𝕂 x) = exp 𝕂 (algebraMap 𝕂 𝔸 x).

LaTeX

$$$ algebraMap 𝕂 𝔸 (exp 𝕂 x) = exp 𝕂 (algebraMap 𝕂 𝔸 x) \quad\text{при } x \in B(0, \operatorname{radius}(\expSeries 𝕂 𝔸))$$$

Lean4

theorem algebraMap_exp_comm_of_mem_ball [CompleteSpace 𝕂] (x : 𝕂)
    (hx : x ∈ EMetric.ball (0 : 𝕂) (expSeries 𝕂 𝕂).radius) : algebraMap 𝕂 𝔸 (exp 𝕂 x) = exp 𝕂 (algebraMap 𝕂 𝔸 x) :=
  map_exp_of_mem_ball _ (continuous_algebraMap 𝕂 𝔸) _ hx

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