mathlib3

58004685 - feat(geometry/manifold/mfderiv): differentiability is a `local_invariant_prop`, and consequences (#15666)

feat(geometry/manifold/mfderiv): differentiability is a `local_invariant_prop`, and consequences (#15666) The boilerplate to make differentiability into a `local_invariant_prop` was missing. I added this, stated the lemmas that the definition of differentiability on a manifold this gives is equivalent to the existing definition, and deduced as a consequence that differentiability is invariant under choice of chart. Almost everything is copied nearly exactly, even up to docstrings, from the corresponding lemmas about `cont_(m)diff`.