Theorems · Theorem · complex analysis

differentiableAt_complex_iff_differentiableAt_real

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

The Cauchy-Riemann Equation: A real-differentiable function f on ℂ is complex-differentiable at x if and only if the derivative fderiv ℝ f x maps I to I • (fderiv ℝ f x) 1.

Defined in

Mathlib.Analysis.Complex.Conformal

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace