mathlib

645dc60f - refactor(analysis/calculus/inverse): inverse of C^k functions over R or C (#5926)

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