mathlib

2b69cd5e - refactor(geometry/manifold/cont_mdiff): split everything about mfderiv (#16982)

refactor(geometry/manifold/cont_mdiff): split everything about mfderiv (#16982) * Remove import `mfderiv` from `cont_mdiff` * Separate everything about `mfderiv` and `mdifferentiable` to a separate file * The reason is that many properties about `mfderiv` are nicely proven once we already know about things like `cont_mdiff_fst` (unless we want to prove `mdifferentiable_fst` separately?) * We could also try to separate out `mdifferentiable` from `mfderiv`. However, this is harder, since proofs about `mdifferentiable` are given using `has_mfderiv_at` * Needed (sort-of) to port more results from the sphere eversion project.