# mathlibdocumentation

analysis.complex.real_deriv

# Real differentiability of complex-differentiable functions #

has_deriv_at.real_of_complex expresses that, if a function on ℂ is differentiable (over ℂ), then its restriction to ℝ is differentiable over ℝ, with derivative the real part of the complex derivative.

### Differentiability of the restriction to ℝ of complex functions #

theorem has_strict_deriv_at.real_of_complex {e : } {e' : } {z : } (h : z) :
has_strict_deriv_at (λ (x : ), (e x).re) e'.re z

If a complex function is differentiable at a real point, then the induced real function is also differentiable at this point, with a derivative equal to the real part of the complex derivative.

theorem has_deriv_at.real_of_complex {e : } {e' : } {z : } (h : e' z) :
has_deriv_at (λ (x : ), (e x).re) e'.re z

If a complex function is differentiable at a real point, then the induced real function is also differentiable at this point, with a derivative equal to the real part of the complex derivative.

theorem times_cont_diff_at.real_of_complex {e : } {z : } {n : with_top } (h : z) :
(λ (x : ), (e x).re) z
theorem times_cont_diff.real_of_complex {e : } {n : with_top } (h : e) :
(λ (x : ), (e x).re)