refactor(algebra/{dual_number,triv_sq_zero_ext}): support non-commuta…

…tive rings (#18384)

This changes the definition of multiplication on `triv_sq_zero_ext R M` as follows
```diff
-x * y = (x.1 * y.1, x.1 • y.2 + y.1 • x.2)
+x * y = (x.1 * y.1, x.1 • y.2 + op y.1 • x.2)
```
which for `R=M` gives the more natural `x.1 * y.2 + x.2 * y.1` in the second term instead of  `x.1 * y.2 + y.1 * x.2`.

This adds some slightly annoying typeclass arguments that could eventually be cleaned up by #10716; but that PR has rotted under the mathlib4 tide. Either way, the weird typeclass arguments needed with `triv_sq_zero_ext R M` are all invisible when working with `dual_number R`.

This is motivated by wanting to talk about `dual_number (quaternion R)` or  `dual_number (matrix n n R)`.

Unfortunately this breaks the `topological_semiring` instance (making it need an `@` and trigger the `fails_quickly` linter), but this instance isn't really interesting anyway.

src/algebra/dual_number.lean

@@ -56,7 +56,7 @@ open triv_sq_zero_ext
 @[simp] lemma snd_eps [has_zero R] [has_one R] : snd ε = (1 : R) := snd_inr _ _
 
 /-- A version of `triv_sq_zero_ext.snd_mul` with `*` instead of `•`. -/
-@[simp] lemma snd_mul [semiring R] (x y : R[ε]) : snd (x * y) = fst x * snd y + fst y * snd x :=
+@[simp] lemma snd_mul [semiring R] (x y : R[ε]) : snd (x * y) = fst x * snd y + snd x * fst y :=
 snd_mul _ _
 
 @[simp] lemma eps_mul_eps [semiring R] : (ε * ε : R[ε]) = 0 := inr_mul_inr _ _ _