Theorem ContinuousLinearMap.toSpanSingleton_zero

Modification history

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