Def ContinuousLinearMap.toSpanSingletonCLE

Modification history

2026-03-31 20:10

Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean

chore: split `Topology.Algebra.Module.StrongTopology` (#37440)

Modified ContinuousLinearMap.toSpanSingletonCLE View on Github →

2025-12-09 14:57

Mathlib/Topology/Algebra/Module/StrongTopology.lean

feat: `toSpanSingleton` as a continuous linear equivalence (#32318) …

Added ContinuousLinearMap.toSpanSingletonCLE View on Github →