Commit 2023-07-13 10:41 cd391184
View on Github →feat(*/prod): prod_prod_prod equivs (#19235)
These send ((a, b), (c, d)) to ((a, c), (b, d)), and this commit provides this bundled as equiv, add_equiv, mul_equiv, ring_equiv, and linear_equiv.
We already have something analogous for tensor_product.