Mathlib v3 is deprecated. Go to Mathlib v4

Theorem complex.has_strict_fderiv_at_exp_real

Modification history

2021-10-23 22:10

src/analysis/special_functions/exp_deriv.lean

refactor(analysis/special_functions/exp_log): split into 4 files (#9882)

Modified complex.has_strict_fderiv_at_exp_real View on Github →

2021-10-04 09:48

src/analysis/special_functions/exp_log.lean

feat(analysis/special_functions): real derivs of `complex.exp` and `complex.log` (#9422)

Added complex.has_strict_fderiv_at_exp_real View on Github →