Commit 2025-06-12 10:16 ea76012f
View on Github →feat: interaction between ContinuousLinearMap.coprod and ContinuousLinearEquiv.prodComm (#25564)
ContinuousLinearMap.coprod_comp_prodComm shows that pre-composition of a coproduct with prodComm swaps the terms in the coproduct. A dependency of #25304.