invOf_exp — Mathlib

English

Let A be a Banach algebra over 𝕂 and x ∈ A with exp(𝕂 x) invertible. Then (exp(𝕂 x))^{-1} = exp(𝕂(-x)).

Русский

Пусть A — банахова алгебра над 𝕂 и x ∈ A так, что exp(𝕂 x) обратимо. Тогда (exp(𝕂 x))^{-1} = exp(𝕂(-x)).

LaTeX

$$$\\left(\\exp 𝕂 x\\right)^{-1} = \\exp 𝕂(-x)$$$

Lean4

theorem invOf_exp (x : 𝔸) [Invertible (exp 𝕂 x)] : ⅟(exp 𝕂 x) = exp 𝕂 (-x) :=
  invOf_exp_of_mem_ball <| (expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _

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