Mathlib v3 is deprecated. Go to Mathlib v4

Def bundle.pullback_total_space_embedding

Modification history

2022-05-29 17:50
src/data/bundle.lean
feat(topology/vector_bundle): the pullback of a vector bundle is a vector bundle (#8545) …
Added bundle.pullback_total_space_embeddingView on Github →