Commit 2022-10-17 11:19 2b69cd5e

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.