Commit 2022-06-02 09:08 57885b4e

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