isUnit_exp

Mathlib.Analysis.Normed.Algebra.Exponential

URI: https://scilib.ai/kg/mathlib#NormedSpace.isUnit_exp

English

For every x, exp(x) is a unit in the algebra; exp(x) has inverse exp(-x).

Русский

Для любого x exp(x) является обратимым элементом алгебры; имеется обратное exp(-x).

LaTeX

$$$\exp 𝕂 x \in 𝔸^{\times}$ and $(\exp 𝕂 x)^{-1} = \exp 𝕂 (-x)$$$

Lean4

theorem isUnit_exp (x : 𝔸) : IsUnit (exp 𝕂 x) :=
  isUnit_exp_of_mem_ball <| (expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru