# Commit 2023-03-28 23:45 01876449

View on Github →feat(geometry/manifold/vector_bundle/tangent): use the new tangent bundle definition in the library (#18601)

- Stop using the old tangent bundle definition, and use the new one instead
- This affects
`geometry.manifold.mfderiv`

and later files. - We remove
`cont_mdiff_at_iff_target`

, which doesn't hold anymore in the new setting. - We prove
`cont_mdiff_at_total_space`

, which characterizes`C^n`

maps into a vector bundle. We need a bunch of basic lemmas to prove this. This makes it easy to prove`smooth_zero_section`

. - We move some results from
`cont_mdiff_mfderiv`

to`manifold/vector_bundle/basic`