Theorem ContinuousLinearMap.toSpanSingleton_comp

Modification history

2026-01-28 18:47
Mathlib/Topology/Algebra/Module/LinearMap.lean
chore(Analysis/LocallyConvex/SeparatingDual): generalize `Algebra.IsCentral.instContinuousLinearMap` (#33351) …
Added ContinuousLinearMap.toSpanSingleton_compView on Github →