hasStrictDerivAt_exp_zero — Mathlib

English

The exponential map has strict derivative 1 at 0; that is, the derivative at 0 is 1.

Русский

У экспоненты строгая производная в нуле равна единице.

LaTeX

$$$$ \dfrac{d}{dz} e^{z} \Big|_{z=0} = 1. $$$$

Lean4

/-- The exponential map in `𝕂 = ℝ` or `𝕂 = ℂ` has strict derivative `1` at zero. -/
theorem hasStrictDerivAt_exp_zero : HasStrictDerivAt (exp 𝕂) (1 : 𝕂) 0 :=
  hasStrictDerivAt_exp_zero_of_radius_pos (expSeries_radius_pos 𝕂 𝕂)

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