mathlib
9dfb9a6e - chore(topology/topological_fiber_bundle): renaming (#8270)

Commit
4 years ago
chore(topology/topological_fiber_bundle): renaming (#8270) In this PR I changed - `prebundle_trivialization` to `topological_fiber_bundle.pretrivialization` - `bundle_trivialization` to `topological_fiber_bundle.trivialization` so to make names consistent with `vector_bundle`. I also changed the name of the file for consistency.
Author
Parents
Loading