mathlib3

f9ec1871 - feat(geometry/manifold/vector_bundle/smooth_section): define smooth sections (#19064)

feat(geometry/manifold/vector_bundle/smooth_section): define smooth sections (#19064) * Define the module of smooth sections of a smooth vector bundle over a smooth manifold. * Co-authored-by: Heather Macbeth [25316162+hrmacbeth@users.noreply.github.com](mailto:25316162+hrmacbeth@users.noreply.github.com) Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>