hasDerivAt_exp — Mathlib

English

For every x in 𝕂, the exponential map exp has derivative at x equal to exp(x).

Русский

Для любого x в 𝕂 экспонента имеет производную в точке x равную exp(x).

LaTeX

$$$$ \dfrac{d}{dz} e^{z} \Big|_{z=x} = e^{x} \quad (x \in \mathbb{K}). $$$$

Lean4

/-- The exponential map in `𝕂 = ℝ` or `𝕂 = ℂ` has derivative `NormedSpace.exp 𝕂 x`
at any point `x`. -/
theorem hasDerivAt_exp {x : 𝕂} : HasDerivAt (exp 𝕂) (exp 𝕂 x) x :=
  hasStrictDerivAt_exp.hasDerivAt

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