Def ContinuousLinearMap.toSpanSingletonLE

Modification history

2025-12-09 14:57
Mathlib/Topology/Algebra/Module/LinearMap.lean
feat: `toSpanSingleton` as a continuous linear equivalence (#32318) …
Added ContinuousLinearMap.toSpanSingletonLEView on Github →