Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-14 22:46 e7386121

View on Github →

feat(analysis/special_functions/exp_deriv): generalize some lemmas about complex.exp, remove *.cexp_real (#13579) Now we can use *.cexp instead of some previous *.cexp_real lemmas.

Estimated changes

modified theorem complex.cont_diff_exp
modified theorem complex.differentiable_exp
modified theorem cont_diff.cexp
modified theorem cont_diff_at.cexp
modified theorem cont_diff_on.cexp
modified theorem cont_diff_within_at.cexp
modified theorem deriv_cexp
modified theorem deriv_within_cexp
modified theorem differentiable.cexp
modified theorem differentiable_at.cexp
modified theorem differentiable_on.cexp
deleted theorem has_deriv_at.cexp_real