Commit 2023-03-28 23:45 01876449

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