chore(analysis/special_functions/exp_deriv): downgrade import (#19139)

Move lemma `complex.is_open_map_exp` from `special_functions/exp_deriv` to right before its (unique) place of use, in `complex.exp_local_homeomorph` in `special_functions/log_deriv`. Morally these belong together: being an open map and being a local homeomorphism are closely tied, they are both consequences of the inverse function theorem and the point of both is to set up being able to differentiate complex log as the inverse function of complex exp. This removes the inverse function theorem from the dependencies of `special_functions/exp_deriv` (a surprisingly widely-imported file).
leanprover-community · Jun 2, 2023 · 6a5c850 · 6a5c850
1 parent 34ebaff
commit 6a5c850
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/src/analysis/special_functions/complex/log_deriv.lean b/src/analysis/special_functions/complex/log_deriv.lean
@@ -3,6 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Benjamin Davidson
 -/
+import analysis.calculus.inverse
 import analysis.special_functions.complex.log
 import analysis.special_functions.exp_deriv
 
@@ -19,6 +20,9 @@ open set filter
 
 open_locale real topology
 
+lemma is_open_map_exp : is_open_map exp :=
+open_map_of_strict_deriv has_strict_deriv_at_exp exp_ne_zero
+
 /-- `complex.exp` as a `local_homeomorph` with `source = {z | -π < im z < π}` and
 `target = {z | 0 < re z} ∪ {z | im z ≠ 0}`. This definition is used to prove that `complex.log`
 is complex differentiable at all points but the negative real semi-axis. -/

diff --git a/src/analysis/special_functions/exp_deriv.lean b/src/analysis/special_functions/exp_deriv.lean
@@ -3,7 +3,6 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne
 -/
-import analysis.calculus.inverse
 import analysis.complex.real_deriv
 
 /-!
@@ -67,9 +66,6 @@ lemma has_strict_fderiv_at_exp_real (x : ℂ) :
   has_strict_fderiv_at exp (exp x • (1 : ℂ →L[ℝ] ℂ)) x :=
 (has_strict_deriv_at_exp x).complex_to_real_fderiv
 
-lemma is_open_map_exp : is_open_map exp :=
-open_map_of_strict_deriv has_strict_deriv_at_exp exp_ne_zero
-
 end complex
 
 section