exp_neg

Mathlib.Analysis.Complex.Exponential

URI: https://scilib.ai/kg/mathlib#Real.exp_neg

English

For real x, exp(-x) = (exp x)^{-1}.

Русский

Для действительного x: exp(-x) = (exp x)^{-1}.

LaTeX

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

Lean4

nonrec theorem exp_neg : exp (-x) = (exp x)⁻¹ :=
  ofReal_injective <| by simp [exp_neg]

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

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

Разделы

Аффилиация

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