Def ContinuousLinearMap.single

Modification history

2025-03-12 03:44
Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean
feat(Topology/): add `Submodule.closure_coe_iSup_map_single` (#22752) …
Added ContinuousLinearMap.singleView on Github →