mathlib

57885b4e - feat(topological_space/vector_bundle): reformulate linearity condition (#14485)

feat(topological_space/vector_bundle): reformulate linearity condition (#14485) * Reformulate the linearity condition on (pre)trivializations of vector bundles using `total_space_mk`. Note: it is definitionally equal to the previous definition, but without using the coercion. * Make one argument of `e.linear` implicit * Simplify the proof of linearity of the product of vector bundles