mathlib3

91b33017 - feat(geometry/manifold/cont_mdiff): add various properties (#16980)

feat(geometry/manifold/cont_mdiff): add various properties (#16980) * More lemmas about `smooth`, more basic lemmas, and some interactions with `cont_diff` and continuous linear maps * Also add various useful lemmas throughout the manifold directory * Add me as author to two files (in `local_invariant_properties` for earlier refactoring PRs) * From the sphere eversion project