exp_add_of_commute — Mathlib

English

HasSum for the inverse factorial weighted expansion equals exp(x): HasSum (n!^{-1} x^n) = exp(x).

Русский

HasSum для весового ряда n!^{-1} x^n равен exp(x).

LaTeX

$$$\text{HasSum } (n !^{-1} x^n) = \exp 𝕂 x$$$

Lean4

/-- In a Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ`, if `x` and `y` commute, then
`NormedSpace.exp 𝕂 (x+y) = (NormedSpace.exp 𝕂 x) * (NormedSpace.exp 𝕂 y)`. -/
theorem exp_add_of_commute {x y : 𝔸} (hxy : Commute x y) : exp 𝕂 (x + y) = exp 𝕂 x * exp 𝕂 y :=
  exp_add_of_commute_of_mem_ball hxy ((expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
    ((expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)

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