Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-28 16:36 645dc60f

View on Github →

refactor(analysis/calculus/inverse): inverse of C^k functions over R or C (#5926) Some results on the local inverse of smooth functions are currently formulated only for real functions, but they work as well for complex functions. We formulate them uniformly, assuming is_R_or_C.

Estimated changes

Modified src/analysis/calculus/inverse.lean

Modified src/analysis/calculus/mean_value.lean

added theorem is_R_or_C.norm_image_sub_le_of_norm_has_fderiv_within_le'

Modified src/analysis/calculus/times_cont_diff.lean

Modified src/analysis/complex/basic.lean

deleted theorem has_deriv_at.real_of_complex

added theorem is_R_or_C.I_to_complex

added theorem is_R_or_C.abs_to_complex

added theorem is_R_or_C.conj_to_complex

added theorem is_R_or_C.im_to_complex

added theorem is_R_or_C.norm_sq_to_complex

added theorem is_R_or_C.re_to_complex

deleted theorem times_cont_diff.real_of_complex

deleted theorem times_cont_diff_at.real_of_complex

Created src/analysis/complex/real_deriv.lean

added theorem has_deriv_at.real_of_complex

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/pow.lean

Modified src/analysis/special_functions/trigonometric.lean

Modified src/data/complex/is_R_or_C.lean

deleted theorem is_R_or_C.I_to_complex

deleted theorem is_R_or_C.abs_to_complex

deleted theorem is_R_or_C.conj_to_complex

deleted theorem is_R_or_C.im_to_complex

deleted theorem is_R_or_C.norm_sq_to_complex

deleted theorem is_R_or_C.re_to_complex

Modified src/geometry/euclidean/basic.lean