Mathlib v3 is deprecated. Go to Mathlib v4

Theorem hom_trivialization_at_target

Modification history

2023-04-25 17:43
src/topology/vector_bundle/hom.lean
feat(topology/vector_bundle/basic): define in_coordinates (#18826) …
Added hom_trivialization_at_targetView on Github →