Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-12 22:46 9dfb9a6e

View on Github →

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.

Estimated changes

deleted structure bundle_trivialization
deleted structure prebundle_trivialization