mathlib

9ac26cb6 - feat(geometry/manifold/mfderiv): derivative of functions between smooth manifolds (#1872)

feat(geometry/manifold/mfderiv): derivative of functions between smooth manifolds (#1872) * feat(geometry/manifold/mfderiv): derivative of functions between smooth manifolds * Update src/geometry/manifold/mfderiv.lean Co-Authored-By: Yury G. Kudryashov <urkud@ya.ru> * more details in docstrings [ci skip] * fix docstrings [ci skip] * reviewer's comments Co-authored-by: Yury G. Kudryashov <urkud@ya.ru>