Def ContinuousLinearMap.coprodEquiv

Modification history

2024-12-23 15:42
Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean
feat: the product of topological modules is a colimit (#20016) …
Added ContinuousLinearMap.coprodEquivView on Github →