exp_neg

Mathlib.Analysis.Complex.Circle

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

English

The negative exponential equals the inverse: exp(-x) = (exp x)^{-1}.

Русский

У экспоненты в знаке минус — обратное: exp(-x) = (exp x)^{-1}.

LaTeX

$$$$ \\exp(-x) = (\\exp x)^{-1}, \\quad x \\in \\mathbb{R}. $$$$

Lean4

@[simp]
theorem exp_neg (x : ℝ) : exp (-x) = (exp x)⁻¹ :=
  expHom.map_neg x

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

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

Разделы

Аффилиация

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