English
If f: ℂ → E is strictly differentiable at x with derivative f', then the real-linear derivative of f at x is given by reCLM.smulRight f' + I · imCLM.smulRight f'.
Русский
Если f: ℂ → E имеет строго дифференцируемость в точке x с производной f', то его реальноподобная производная равна reCLM.smulRight f' + I · imCLM.smulRight f'.
LaTeX
$$$\displaystyle \text{If } f: \mathbb{C} \to E \text{ is strictly differentiable at } x \text{ with } f', \text{ then } Df(x) = \Re\!\operatorname{CLM}(f') + i\Im\!\operatorname{CLM}(f').$$$
Lean4
theorem complexToReal_fderiv' {f : ℂ → E} {x : ℂ} {f' : E} (h : HasStrictDerivAt f f' x) :
HasStrictFDerivAt f (reCLM.smulRight f' + I • imCLM.smulRight f') x := by
simpa only [Complex.restrictScalars_one_smulRight'] using h.hasStrictFDerivAt.restrictScalars ℝ
