mathlib3

b8d2eaa6 - refactor(algebra/{dual_number,triv_sq_zero_ext}): support non-commutative rings (#18384)

refactor(algebra/{dual_number,triv_sq_zero_ext}): support non-commutative 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.