exp_neg — Mathlib

English

Exponential of a negated argument equals the inverse of the exponential: exp(-x) = (exp x)^{-1}.

Русский

Экспонента при отрицательном аргументе равна обратному экспоненте: exp(-x) = (exp x)^{-1}.

LaTeX

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

Lean4

theorem exp_neg (x : EReal) : exp (-x) = (exp x)⁻¹ := by
  induction x
  · simp
  · rw [exp_coe, ← EReal.coe_neg, exp_coe, ← ENNReal.ofReal_inv_of_pos (Real.exp_pos _), Real.exp_neg]
  · simp

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