Commit 2026-10-11 08:58 1619863c

feat: add ContMDiffWithinAt.contMDiffWithinAt_tangentMapWithin and friends (#44710) This is basically extracting the current proof into a sub-lemma, and filling in the API gaps. These lemmas are used to prove that mvfderiv of a smooth function into a normed space is smooth: #44711. That in turn is used to define the curvature tensor. From the Riemannian geometry project.