Theorems · Theorem · complex analysis

HasFDerivWithinAt.complexOfReal

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {x : ℂ} {s : Set ℂ}
  {f' : ℂ →L[ℝ] E},
  HasFDerivWithinAt f f' s x → ∀ (h₂ : f' Complex.I = Complex.I • f' 1), HasFDerivWithinAt f (f'.complexOfReal h₂) s x

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

Defined in

Mathlib.Analysis.Complex.Conformal

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace