Partial completion of #855

[kastch]

Addresses #855

Added Time.manifoldDeriv in SpaceAndTime/Time/Derivatives.lean: the derivative of a function from Time to a manifold, valued in the tangent space.

Added Time.manifoldDeriv_eq, Time.deriv_eq_mfderiv, Time.deriv_eq_manifoldDeriv, and Time.manifoldDeriv_const in SpaceAndTime/Time/Derivatives.lean: basic API relating manifoldDeriv to mfderiv and to the existing Time.deriv for normed-space targets.

[github-actions]

Thank you for this PR, which will now be reviewed.
If submitting to ./Physlib or ./QuantumInfo, please
see our review guidelines
if you are not familiar with the process. You should expect a back and forth
with a reviewer before your PR is merged. See also that link for how to
add appropriate labels to your PR. The PR will also go through a number
of automated checks. You can learn more about these here,
including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process,
though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this
thread of the Lean Zulip.

[jstoobysmith]

One small comment about vadd results. I will add awaiting-author label. Please can you comment with -awaiting-author when responded (helps with review organization).

[jstoobysmith]

Not clear to me why these lemmas in this file are needed.

[kastch]

Hi @jstoobysmith ! Agreed - added more a draft ones rather then real closing for the second thing. I'll address it in a full API way in a separate PR later. In this one - removed those.

[kastch]

-awaiting-author

[jstoobysmith]

Approved - many thanks!