English
A complex function is differentiable at a point iff it is differentiable as a real function with a CR relation on the derivative.
Русский
Комплексная функция дифференцируема в точке тогда и только тогда, когда она дифференцируема как вещественная функция с CR‑отношением на производной.
LaTeX
$$DifferentiableAt ℂ f x \iff (DifferentiableAt Real f x) ∧ (fderiv Real f x I = I • fderiv Real f x 1)$$
Lean4
/-- 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`.
-/
theorem differentiableAt_complex_iff_differentiableAt_real :
DifferentiableAt ℂ f x ↔ DifferentiableAt ℝ f x ∧ fderiv ℝ f x I = I • fderiv ℝ f x 1 :=
⟨fun h ↦ by simp [h.restrictScalars ℝ, h.fderiv_restrictScalars ℝ], fun ⟨h₁, h₂⟩ ↦
(differentiableAt_iff_restrictScalars ℝ h₁).2 ⟨(fderiv ℝ f x).complexOfReal h₂, rfl⟩⟩
