Theorem MDifferentiableWithinAt.compContinuousAlternatingMapCLM

Modification history

2026-10-13 11:38
Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
feat: alternating maps and associated operations are `ContMDiff` and `MDifferentiable` (#44371) …
Added MDifferentiableWithinAt.compContinuousAlternatingMapCLMView on Github →