mathlib3

15e8bc48 - feat(topology/vector_bundle): define pretrivialization.symm (#14192)

feat(topology/vector_bundle): define pretrivialization.symm (#14192) * Also adds some other useful lemmas about (pre)trivializations * This splits out the part of #8545 that is unrelated to pullbacks - Co-authored by Nicolo Cavalleri <nico@cavalleri.net>