mathlib

ddec54a7 - feat(geometry/manifold/vector_bundle/tangent): the tangent bundle is a smooth vector bundle (#17680)

feat(geometry/manifold/vector_bundle/tangent): the tangent bundle is a smooth vector bundle (#17680) * This defines a tangent bundle as a smooth vector bundle * Currently we still use the old definition in the library (e.g. for `mfderiv`). Therefore we put the new version temporarily in the `hidden` namespace, to avoid a name clash (we could skip this PR and immediately merge #18068, but that will be a big PR). Co-authored by: Heather Macbeth 25316162+hrmacbeth@users.noreply.github.com Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>