mathlib documentation


Dual quaternions #

Similar to the way that rotations in 3D space can be represented by quaternions of unit length, rigid motions in 3D space can be represented by dual quaternions of unit length.

Main results #

References #

The dual quaternions can be equivalently represented as a quaternion with dual coefficients, or as a dual number with quaternion coefficients.

See also matrix.dual_number_equiv for a similar result.


Lemmas characterizing quaternion.dual_number_equiv.