mathlib

2bde21d1 - feat(geometry/manifold/times_cont_mdiff): API for checking `times_cont_mdiff` (#5631)

feat(geometry/manifold/times_cont_mdiff): API for checking `times_cont_mdiff` (#5631) Two families of lemmas: - to be `times_cont_mdiff`, it suffices to be `times_cont_mdiff` after postcomposition with any chart of the target - projection notation to go from `times_cont_diff` (in a vector space) to `times_cont_mdiff`