Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes