mathlib

55f32dae - feat(topology/vector_bundle): the pullback of a vector bundle is a vector bundle (#8545)

feat(topology/vector_bundle): the pullback of a vector bundle is a vector bundle (#8545) We construct the pullback bundle of a vector bundle. * Co-authored by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> * Co-authored by: Floris van Doorn <fpvdoorn@gmail.com> * Co-authored by: Sebastien Gouezel <sebastien.gouezel@univ-rennes1.fr>