Local diffeomorphism PRs

Stream: PR reviews

[Michael Rothgang]

#8738 is ready for review again: it proves that the differential of a local diffeomorphism is a continuous linear equivalence.

[Michael Rothgang]

The PR itself is over a year and was blocked on a design question for a long time. That question has a satisfactory solution (which was merged in #23219); the remaining PR should be straightforward (and is just 90 lines).

[Michael Rothgang]

#9273 builds on that and can be used to prove that extended charts are local diffeomorphisms at each interior point. (Right now, it proves something slightly weaker.) Is that a useful result, despite not working at boundary points? (I certainly aim to show something about boundary points also, but that requires a different approach.)