Commit 2020-11-22 12:03 a6498516

View on Github →

chore(analysis/complex/basic): add times_cont_diff.real_of_complex (#5073) Also rename has_deriv_at_real_of_complex to has_deriv_at.real_of_complex.

Estimated changes

Modified src/analysis/complex/basic.lean

added theorem has_deriv_at.real_of_complex

deleted theorem has_deriv_at_real_of_complex

deleted theorem has_deriv_at_real_of_complex_aux

added theorem times_cont_diff.real_of_complex

added theorem times_cont_diff_at.real_of_complex

Modified src/analysis/special_functions/exp_log.lean

Modified src/analysis/special_functions/trigonometric.lean