English
If f: ℂ → E is differentiable at x with derivative f', then the real-linear derivative of f at x is f' real-linear combination 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 differentiable at } x \text{ with } f',\ \mathrm{D}f(x) = \mathrm{reCLM}.smulRight(f') + i \mathrm{imCLM}.smulRight(f').$$$
Lean4
theorem complexToReal_fderiv' {f : ℂ → E} {x : ℂ} {f' : E} (h : HasDerivAt f f' x) :
HasFDerivAt f (reCLM.smulRight f' + I • imCLM.smulRight f') x := by
simpa only [Complex.restrictScalars_one_smulRight'] using h.hasFDerivAt.restrictScalars ℝ
