exp_add — Mathlib

English

In a commutative Banach-algebra, exp(x+y) = exp(x) exp(y).

Русский

В коммутативной банаховой алгебре exp(x+y) = exp(x) exp(y).

LaTeX

$$$\\exp 𝕂 (x+y) = \\exp 𝕂 x \\; \\exp 𝕂 y$$$

Lean4

/-- In a commutative Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ`,
`NormedSpace.exp 𝕂 (x+y) = (NormedSpace.exp 𝕂 x) * (NormedSpace.exp 𝕂 y)`. -/
theorem exp_add {x y : 𝔸} : exp 𝕂 (x + y) = exp 𝕂 x * exp 𝕂 y :=
  exp_add_of_mem_ball ((expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
    ((expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)

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