mathlib

0575db0c - feat(topology/vector_bundle): define some useful linear maps globally (#14484)

feat(topology/vector_bundle): define some useful linear maps globally (#14484) * Define `pretrivialization.symmₗ`, `pretrivialization.linear_map_at`, `trivialization.symmL`, `trivialization.continuous_linear_map_at` * These are globally-defined (continuous) linear maps. They are linear equivalences on `e.base_set`, but it is useful to define these globally. They are defined as `0` outside `e.base_set` * These are convenient to define the vector bundle of continuous linear maps. Co-authored-by: Patrick Massot <patrickmassot@free.fr>