English
If e is differentiable at Complex.ofReal(z) with derivative e', then the restriction x ↦ e(x) to ℝ composed by Complex.ofReal is differentiable at z with the same derivative e'.
Русский
Если e дифференцируема в Complex.ofReal(z) с производной e', то ограничение x ↦ e(Complex.ofReal x) на ℝ дифференцируемо в z с той же производной.
LaTeX
$$$\displaystyle \text{If } h: \text{HasDerivAt } e e' (\mathsf{Complex}.ofReal z), \text{ then } x \mapsto e(\mathsf{Complex}.ofReal x) \text{ has derivative } e'\text{ at } z.$$$
Lean4
/-- If a complex function `e` is differentiable at a real point, then its restriction to `ℝ` is
differentiable there as a function `ℝ → ℂ`, with the same derivative. -/
theorem comp_ofReal (hf : HasDerivAt e e' ↑z) : HasDerivAt (fun y : ℝ => e ↑y) e' z := by
simpa only [ofRealCLM_apply, ofReal_one, mul_one] using hf.comp z ofRealCLM.hasDerivAt
