Theorem ContinuousAlternatingMap.tsum_eval

Modification history

2025-11-25 10:20

Mathlib/Topology/Algebra/Module/Alternating/Topology.lean

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

Modified ContinuousAlternatingMap.tsum_eval View on Github →

2024-09-08 21:52

Mathlib/Topology/Algebra/Module/Alternating/Topology.lean

feat: topology on `ContinuousAlternatingMap`s (#16374)

Added ContinuousAlternatingMap.tsum_eval View on Github →