Theorem mdifferentiableAt_apply

Modification history

2026-10-13 11:38

Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean

feat: alternating maps and associated operations are `ContMDiff` and `MDifferentiable` (#44371) …

Added mdifferentiableAt_apply View on Github →