Theorem ContinuousLinearMap.coprod_comp_prodComm

Modification history

2026-08-13 20:38
Mathlib/Topology/Algebra/Module/Equiv.lean
chore: split `ContinuousLinearMap.IsInvertible` to its own file (#42697) …
Modified ContinuousLinearMap.coprod_comp_prodCommView on Github →
2025-06-12 10:16
Mathlib/Topology/Algebra/Module/Equiv.lean
feat: interaction between ContinuousLinearMap.coprod and ContinuousLinearEquiv.prodComm (#25564) …
Added ContinuousLinearMap.coprod_comp_prodCommView on Github →