Commit 2025-03-25 13:29 74053d08

feat: local inverse of a diffeomorphism (#23219) Add IsLocalDiffeomorphAt.localInverse, a (choice of) local inverse for a local diffeomorphism at x. Prove basic API about it: if f is a local diffeomorphism at x, we prove that

• f and its local inverse near x are local inverses (in both directions),
• composing f and its local inverse is EventuallyEq to the identity near x.
• smoothness results for the local inverse. PR #8738 will use this to prove that the differential of a local diffeomorphism is a continuous linear equivalence.