mathlib

536c256e - feat(algebra/dual_quaternion): two equivalent ways to construct the dual quaternions (#18383)

feat(algebra/dual_quaternion): two equivalent ways to construct the dual quaternions (#18383) We show that the dual numbers with quaternion coefficients are isomorphic as an algebra to the quaternions with dual number coefficients. The result is trivial, but being able to state it turned out to require generalizations of existing typeclass instances, which are handled in prework PRs. This is very similar to #18386.