search

leanprover-community / mathlib

Lean 3's obsolete mathematical components library: please use mathlib4
https://leanprover-community.github.io/lean3
Apache License 2.0
1.66k stars 297 forks source link

[Merged by Bors] - feat(*/prod): `prod_prod_prod` equivs #19235

Closed eric-wieser closed 12 months ago

eric-wieser commented 12 months ago

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.

Open in Gitpod

Split from #18447

fpvandoorn commented 12 months ago

LGTM

bors d+

bors[bot] commented 12 months ago

:v: eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

eric-wieser commented 12 months ago

bors merge

bors[bot] commented 12 months ago

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here. For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.