[Merged by Bors] - chore(Algebra/DualNumber): ε commutes

[eric-wieser]

This doesn't generalize to TrivSqZeroExt, as we do not have a notion of Commute for smul.

---

[ocfnash]

I note that we already have:

example [CommSemiring R] : CommSemiring (DualNumber R) := inferInstance -- Uses `TrivSqZeroExt.commSemiring`

bors merge

[eric-wieser]

Indeed, though the result in this PR works for Semiring R as opposed to CommSemiring R!

[ocfnash]

Indeed, though the result in this PR works for Semiring R as opposed to CommSemiring R!

Of course, I realise this: hence I merged it.

What I was trying to say with my comment was "I was going to suggest we add this other commutativity fact [that everything commutes if the scalars commute] but I found it was already there, so I think these results are the only missing pieces and should just be merged".

[eric-wieser]

so I think these results are the only missing pieces

I thought this too but then #7934 happened!

[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