hasDerivAt_exp_zero

Mathlib.Analysis.SpecialFunctions.Exponential

URI: https://scilib.ai/kg/mathlib#hasDerivAt_exp_zero

← MathLib Explorer

English

The exponential map exp has derivative 1 at zero, i.e., exp'(0) = 1.

Русский

У экспоненты в нуле производная равна единице: exp'(0) = 1.

LaTeX

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

Lean4

/-- The exponential map in `𝕂 = ℝ` or `𝕂 = ℂ` has derivative `1` at zero. -/
theorem hasDerivAt_exp_zero : HasDerivAt (exp 𝕂) (1 : 𝕂) 0 :=
  hasStrictDerivAt_exp_zero.hasDerivAt

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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