[Merged by Bors] - feat: product instances for OrderedSub

[semorrison]

---

[ocfnash]

Surely these instances could go in Mathlib.Algebra.Order.Sub.Basic?

I'm generally in favour of smaller files but in this case the granularity seems a bit too fine. I note that though you import Sub.Canonical, in fact Sub.Basic suffices.

In any case, I'll let you decide.

bors d+

[bors]

✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[semorrison]

Surely these instances could go in Mathlib.Algebra.Order.Sub.Basic?

I'm generally in favour of smaller files but in this case the granularity seems a bit too fine. I note that though you import Sub.Canonical, in fact Sub.Basic suffices.

In any case, I'll let you decide.

bors d+

Unfortunately in Sub.Basic we fail with: error: failed to synthesize instance Add (α × β)

[semorrison]

bors merge

[bors]

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.

• Build
• Check all files imported
• Lint style