Theorem ContinuousLinearMap.coprod_comp_inr

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_comp_inrView on Github →