English
If f: ℂ → ℂ has a strict derivative at x with derivative f', then its real-linear derivative is f' acting via the decomposition into real and imaginary parts.
Русский
Если у f: ℂ → ℂ есть строгая производная в точке x с производной f', то её реальноподобная производная выражается через разложение на действительную и мнимую части.
LaTeX
$$$\displaystyle \text{If } f: \mathbb{C} \to \mathbb{C} \text{ has a strict derivative at } x \text{ with } f',\ \text{then } Df(x)= f'\Re\,+ i f'\Im.$$$
Lean4
theorem complexToReal_fderiv' {f : ℂ → E} {s : Set ℂ} {x : ℂ} {f' : E} (h : HasDerivWithinAt f f' s x) :
HasFDerivWithinAt f (reCLM.smulRight f' + I • imCLM.smulRight f') s x := by
simpa only [Complex.restrictScalars_one_smulRight'] using h.hasFDerivWithinAt.restrictScalars ℝ
