Theorems · Theorem · complex analysis

complexOfReal_deriv

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {x : ℂ},
  DifferentiableAt ℝ f x → (fderiv ℝ f x) Complex.I = Complex.I • (fderiv ℝ f x) 1 → deriv f x = (fderiv ℝ f x) 1

In cases where the Cauchy-Riemann Equation guarantees complex differentiability at x, the complex derivative equals the real derivative.

Defined in

Mathlib.Analysis.Complex.Conformal

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace