Theorem MDifferentiableWithinAt.cle_arrowCongr

Modification history

2024-11-28 15:29
Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
feat: manifold derivative of operations in vector spaces (#18849) …
Added MDifferentiableWithinAt.cle_arrowCongrView on Github →