Mathlib v3 is deprecated. Go to Mathlib v4

Theorem bundle.total_space.mk_cast

Modification history

2022-05-23 14:09
src/data/bundle.lean
feat(topology/vector_bundle): define pretrivialization.symm (#14192) …
Added bundle.total_space.mk_castView on Github →