Theorems · Theorem · complex analysis

HasDerivAt.real_of_complex

∀ {e : ℂ → ℂ} {e' : ℂ} {z : ℝ}, HasDerivAt e e' ↑z → HasDerivAt (fun x => (e ↑x).re) e'.re z

If a complex function e is differentiable at a real point, then the function ℝ → ℝ given by the real part of e is also differentiable at this point, with a derivative equal to the real part of the complex derivative.

Defined in

Mathlib.Analysis.Complex.RealDeriv

Cited by

7 results in Mathlib

Foundations

Depth 169 from the axioms · uses propext, Classical.choice, Quot.sound