deriv_cexp

Mathlib.Analysis.SpecialFunctions.ExpDeriv

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

← MathLib Explorer

English

The derivative of exp is exp itself, i.e., deriv(exp) = exp.

Русский

Производная exp равна exp: deriv(exp) = exp.

LaTeX

$$$ \\operatorname{deriv}(\\exp) = \\exp$$$

Lean4

@[simp]
theorem deriv_cexp (hc : DifferentiableAt 𝕜 f x) :
    deriv (fun x => Complex.exp (f x)) x = Complex.exp (f x) * deriv f x :=
  hc.hasDerivAt.cexp.deriv

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

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

Разделы

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

Аффилиация

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