complexToReal_fderiv — Mathlib

English

If f: ℂ → E is strictly differentiable at x with derivative f', then the real-linear derivative equals reCLM.smulRight f' + I • imCLM.smulRight f'.

Русский

Если f: ℂ → E строго дифференцируема в x с производной f', тогда реальная линейная производная равна reCLM.smulRight f' + I • imCLM.smulRight f'.

LaTeX

$$$\displaystyle Df(x) = \operatorname{reCLM}.smulRight(f') + i \operatorname{imCLM}.smulRight(f').$$$

Lean4

theorem complexToReal_fderiv {f : ℂ → ℂ} {f' x : ℂ} (h : HasDerivAt f f' x) : HasFDerivAt f (f' • (1 : ℂ →L[ℝ] ℂ)) x :=
  by simpa only [Complex.restrictScalars_one_smulRight] using h.hasFDerivAt.restrictScalars ℝ

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