isUnit_exp_of_mem_ball — Mathlib

English

Let the exponential series converge at x (i.e., x lies inside the radius of convergence). Then exp(x) is a unit in the algebra; equivalently, exp(x) has a multiplicative inverse.

Русский

Пусть экспоненциальная сумма сходится в точке x (x лежит внутри радиуса сходимости). Тогда exp(x) является обратимым элементом в алгебре; то есть у него существует обратный элемент по умножению.

LaTeX

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

Lean4

theorem isUnit_exp_of_mem_ball [CharZero 𝕂] {x : 𝔸} (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
    IsUnit (exp 𝕂 x) :=
  @isUnit_of_invertible _ _ _ (invertibleExpOfMemBall hx)

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