mathlib
cd391184 - feat(*/prod): `prod_prod_prod` equivs (#19235)

Commit
2 years ago
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`.
Author
Parents
Loading