cexp — Mathlib

English

The strict Fréchet derivative of exp at x is exp(x) times the identity on ℂ viewed as a real vector space.

Русский

Строгая Фрете производная exp в x равна exp(x) умноженной на тождественную карту на ℂ как вещественное пространство.

LaTeX

$$$ HasStrictFDerivAt(\\exp, \\exp(x) \\cdot \\mathrm{Id}_{\\mathbb{C}}, x) $$$

Lean4

theorem cexp (hf : HasStrictFDerivAt f f' x) :
    HasStrictFDerivAt (fun x => Complex.exp (f x)) (Complex.exp (f x) • f') x :=
  (Complex.hasStrictDerivAt_exp (f x)).comp_hasStrictFDerivAt x hf

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