tangent_bundle): the `tangent_bundle` is a `topological_vector_bundle` (#8295)

Commit

3 years ago

feat(geometry/manifold/tangent_bundle): the `tangent_bundle` is a `topological_vector_bundle` (#8295) Co-authored-by: Patrick Massot <patrickmassot@free.fr>

Author

Nicknamen

Parents

a19f6c6f

mathlib f063d0c6 - feat(geometry/manifold/tangent_bundle): the `tangent_bundle` is a `topological_vector_bundle` (#8295)

mathlib
f063d0c6 - feat(geometry/manifold/tangent_bundle): the `tangent_bundle` is a `topological_vector_bundle` (#8295)