expSeries_hasSum_exp_of_mem_ball — Mathlib

English

If x and y commute, then exp(x+y) = exp(x) exp(y) (under suitable convergence).

Русский

Если x и y коммутируют, тогда exp(x+y) = exp(x) exp(y) при надлежащей сходимости.

LaTeX

$$ExpCommuteAdd x y$$

Lean4

theorem expSeries_hasSum_exp_of_mem_ball (x : 𝔸) (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
    HasSum (fun n => expSeries 𝕂 𝔸 n fun _ => x) (exp 𝕂 x) :=
  FormalMultilinearSeries.hasSum (expSeries 𝕂 𝔸) hx

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