Theorem ContinuousLinearMap.comp_coprod

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.comp_coprodView on Github →