mathlib

d939b0e6 - feat(topology/vector_bundle/hom): define the vector bundle of continuous linear maps (#14541)

feat(topology/vector_bundle/hom): define the vector bundle of continuous linear maps (#14541) * The changes in `topology/fiber_bundle` are not necessary for this PR, but perhaps nice additions * Co-authored by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> * Co-authored by: Patrick Massot <patrick.massot@u-psud.fr> Co-authored-by: Patrick Massot <patrickmassot@free.fr>