Theorem ContinuousLinearMap.intrinsicStar_toSpanSingleton

Modification history

2026-02-18 12:06

Mathlib/Topology/Algebra/Star/LinearMap.lean

feat(Topology/Algebra/Star/LinearMap): intrinsic star for continuous linear maps (#33397)

Added ContinuousLinearMap.intrinsicStar_toSpanSingleton View on Github →