mathlib

8e57ff9a - feat(geometry/manifold/cont_mdiff): local structomorphisms of `cont_diff_groupoid` (#17291)

feat(geometry/manifold/cont_mdiff): local structomorphisms of `cont_diff_groupoid` (#17291) Let `M` and `M'` be smooth manifolds with the same model-with-corners, `I`. Then `f : M → M'` is a local structomorphism for `I`, if and only if it is manifold-smooth on the domain of definition in both directions. Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>