mathlib
a312e7e2 - chore(topology/topological_fiber_bundle): reorganizing the code (#7938)

Commit
4 years ago
chore(topology/topological_fiber_bundle): reorganizing the code (#7938) What I do here: - Get rid of `local_triv`: it is not needed. - Change `local_triv_ext` to `local_triv` - Rename `local_triv'` as `local_triv_as_local_equiv` (name suggested by @sgouezel) - Improve type class inference by getting rid of `dsimp` in instances - Move results about `bundle` that do not need the topology in an appropriate file - Update docs accordingly. Nothing else. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Author
Parents
Loading