Def ContinuousAlternatingMap.fderivCompContinuousLinearMap

Modification history

2025-11-25 10:20

Mathlib/Analysis/Normed/Module/Alternating/Basic.lean

feat(Calculus): derivative of `ContinuousAlternatingMap.compContinuousLinearMap` (#30331)

Added ContinuousAlternatingMap.fderivCompContinuousLinearMap View on Github →