mathlib

b1ca33e0 - feat(analysis/calculus/times_cont_diff, analysis/calculus/inverse): smooth inverse function theorem (#4407)

feat(analysis/calculus/times_cont_diff, analysis/calculus/inverse): smooth inverse function theorem (#4407) The inverse function theorem, in the C^k and smooth categories. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>