Theorem ContinuousLinearMap.coprod_add

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