Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-04 09:48 b6f94a93

View on Github →

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

Estimated changes

Modified src/analysis/complex/basic.lean

added theorem complex.restrict_scalars_one_smul_right'

added theorem complex.restrict_scalars_one_smul_right

Modified src/analysis/complex/real_deriv.lean

added theorem has_deriv_at.complex_to_real_fderiv'

added theorem has_deriv_at.complex_to_real_fderiv

added theorem has_deriv_within_at.complex_to_real_fderiv'

added theorem has_deriv_within_at.complex_to_real_fderiv

added theorem has_strict_deriv_at.complex_to_real_fderiv'

added theorem has_strict_deriv_at.complex_to_real_fderiv

Modified src/analysis/special_functions/complex/log.lean

added theorem complex.has_strict_fderiv_at_log_real

added theorem has_deriv_at.clog_real

added theorem has_deriv_within_at.clog_real

added theorem has_strict_deriv_at.clog_real

Modified src/analysis/special_functions/exp_log.lean

added theorem complex.has_strict_fderiv_at_exp_real

added theorem has_deriv_at.cexp_real

added theorem has_deriv_within_at.cexp_real

added theorem has_strict_deriv_at.cexp_real