Commit 2023-06-02 04:32 6a5c8500

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).