Commit 2022-11-10 09:01 0b00e53a

chore(topology/fiber_bundle): move trivializations to a new file (#17463) Split the file topology.fiber_bundle into two, topology.fiber_bundle.trivialization and topology.fiber_bundle.basic, the former treating (pre)trivializations and the latter treating fiber bundles and constructions for them (the core construction, the prebundle construction, etc). Also move lemmas from topology.vector_bundle.basic which turned out not to invove the linear structure (cf this discussion) into topology.fiber_bundle.trivialization.