invOf_exp_of_mem_ball — Mathlib

English

If x lies in the ball of convergence, then the multiplicative inverse of exp(x) is exp(-x).

Русский

Если x лежит в шаре предельной области, то обратное exp(x) равно exp(-x).

LaTeX

$$$ x \in B(0, \operatorname{radius}(\expSeries 𝕂 𝔸)) \Rightarrow (\exp 𝕂 x)^{-1} = \exp 𝕂 (-x)$$$

Lean4

theorem invOf_exp_of_mem_ball [CharZero 𝕂] {x : 𝔸} (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius)
    [Invertible (exp 𝕂 x)] : ⅟(exp 𝕂 x) = exp 𝕂 (-x) := by letI := invertibleExpOfMemBall hx;
  convert (rfl : ⅟(exp 𝕂 x) = _)

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