Commit 2025-07-27 15:33 6636c971

View on Github →

feat: implement the Cauchy-Riemann Equation (#26839) Describe complex differentiability for functions f : ℂ → ℂ using the Cauchy-Riemann equation. This material closes a long-standing open TODO. It is used in Project VD, which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. It is one of the ingredients in the proof of Jensen's Formula in complex analysis.

Estimated changes

Modified Mathlib/Analysis/Complex/Conformal.lean

added theorem ContinuousLinearMap.coe_complexOfReal

added def ContinuousLinearMap.complexOfReal

added theorem LinearMap.coe_complexOfReal

added def LinearMap.complexOfReal

added theorem complexOfReal_deriv

added theorem complexOfReal_derivWithin

added theorem complexOfReal_fderiv

added theorem complexOfReal_fderivWithin

added theorem complexOfReal_hasDerivAt

added theorem complexOfReal_hasDerivWithinAt

added theorem differentiableAt_complex_iff_differentiableAt_real

added theorem differentiableWithinAt_complex_iff_differentiableWithinAt_real

added theorem real_linearMap_map_smul_complex