mathlib

be2c24f5 - feat(geometry/manifold/vector_bundle/basic): smooth vector bundles (#17611)

feat(geometry/manifold/vector_bundle/basic): smooth vector bundles (#17611) Definition of smooth vector bundle, and basic constructions (direct sum, pullback, core construction). Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com> Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>