Commit 2023-02-23 11:46 b8d2eaa6

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

-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.