Theorem ContinuousAlternatingMap.compContinuousLinearMapCLM_apply

Modification history

2026-03-06 01:12
Mathlib/Analysis/Normed/Module/Alternating/Basic.lean
feat(ContinuousAlternatingMap): generalize some definitions (#34513)
Deleted ContinuousAlternatingMap.compContinuousLinearMapCLM_applyView on Github →
2025-11-26 01:45
Mathlib/Analysis/Normed/Module/Alternating/Basic.lean
feat(DifferentialForm): pullback commutes with exterior derivative (#30871)
Added ContinuousAlternatingMap.compContinuousLinearMapCLM_applyView on Github →