inverse_exp

Mathlib.Analysis.Normed.Algebra.Exponential

URI: https://scilib.ai/kg/mathlib#Ring.inverse_exp

English

In a Banach algebra over 𝕂, exp(x) is invertible and its inverse equals exp(-x).

Русский

В банаховой алгебре над 𝕂 экспонента exp(x) обратима, и её обратный элемент равен exp(-x).

LaTeX

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

Lean4

theorem _root_.Ring.inverse_exp (x : 𝔸) : Ring.inverse (exp 𝕂 x) = exp 𝕂 (-x) :=
  letI := invertibleExp 𝕂 x
  Ring.inverse_invertible _

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

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

Разделы

Аффилиация

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