mathlib3

2f516593 - feat(analysis/special_functions/exp_log): `exp` is infinitely smooth (#5086)

feat(analysis/special_functions/exp_log): `exp` is infinitely smooth (#5086) * Prove that `complex.exp` and `real.exp` are infinitely smooth. * Generalize lemmas about `exp ∘ f` to `f : E → ℂ` or `f : E → ℝ` instead of `f : ℂ → ℂ` or `f : ℝ → ℝ`.