Commit 2026-02-23 22:55 8b62eaae
View on Github →feat: add (m)differentiableAt_of_(m)fderiv_injective (#35284)
and versions for (m)fderivWithin versions. This generalises the existing lemmas (m)differentiableAt_of_isInvertible_(m)fderiv and friends.
Extracted from #35078; from the path to immersions, embeddings and submanifolds.