Commit 2023-06-04 13:34 abdf755c

View on Github →

feat: port Analysis.Complex.RealDeriv (#4642)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Complex/RealDeriv.lean

added theorem ContDiff.real_of_complex

added theorem ContDiffAt.real_of_complex

added theorem DifferentiableAt.conformalAt

added theorem HasDerivAt.comp_of_real

added theorem HasDerivAt.complexToReal_fderiv'

added theorem HasDerivAt.complexToReal_fderiv

added theorem HasDerivAt.of_real_comp

added theorem HasDerivAt.real_of_complex

added theorem HasDerivWithinAt.complexToReal_fderiv'

added theorem HasDerivWithinAt.complexToReal_fderiv

added theorem HasStrictDerivAt.complexToReal_fderiv'

added theorem HasStrictDerivAt.complexToReal_fderiv

added theorem HasStrictDerivAt.real_of_complex

added theorem conformalAt_iff_differentiableAt_or_differentiableAt_comp_conj