Commit 2020-01-17 03:02 9ac26cb6
View on Github →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