2025-11-25 10:20
Mathlib/Analysis/Normed/Module/Alternating/Basic.lean
feat(Calculus): derivative of `ContinuousAlternatingMap.compContinuousLinearMap` (#30331)
Added ContinuousAlternatingMap.toContinuousMultilinearMapCLM_comp_fderivCompContinuousLinearMap