Commit 2026-08-20 12:42 d67241ee

chore: fix defeq abuse in the definition of MFDeriv (#42193) The current definition of the manifold derivative relies on wild defeq abuse between the tangent space at a point and the model space. This PR introduces continuous linear maps making these identifications explicit, and uses them to avoid the defeq abuse in the definitions. The goal of this PR is not to fix all the defeq abuses: when dealing with vector spaces, the fact that one can transparently identify a vector space and the tangent space to the vector space is a feature of the implementation, not a defect.