Theorem ContinuousAlternatingMap.continuous_compContinuousLinearMapCLM

Modification history

2026-03-06 01:12
Mathlib/Analysis/Normed/Module/Alternating/Basic.lean
feat(ContinuousAlternatingMap): generalize some definitions (#34513)
Added ContinuousAlternatingMap.continuous_compContinuousLinearMapCLMView on Github →