Theorem DifferentiableWithinAt.continuousAlternatingMapCompContinuousLinearMap

Modification history

2025-11-25 10:20
Mathlib/Analysis/Calculus/FDeriv/ContinuousAlternatingMap.lean
feat(Calculus): derivative of `ContinuousAlternatingMap.compContinuousLinearMap` (#30331)
Added DifferentiableWithinAt.continuousAlternatingMapCompContinuousLinearMapView on Github →