English
One can view dual quaternions either as quaternions with dual-number coefficients or as dual numbers with quaternion coefficients.
Русский
Двойные кватернионы можно рассматривать либо как кватерионы с двойночленными коэффициентами, либо как двойные числа с кватернионными коэффициентами.
LaTeX
$$$\text{dualNumberEquiv} : \text{Quaternion}(\text{DualNumber } R) \simeq_A[R] \text{DualNumber}(\text{Quaternion } R)$$$
Lean4
/-- Show DualNumber with values x and y as an "x + y*ε" string -/
instance instRepr [Repr R] : Repr (DualNumber R) where
reprPrec f
p :=
(if p > 65 then (Std.Format.bracket "(" · ")") else (·)) <| reprPrec f.fst 65 ++ " + " ++ reprPrec f.snd 70 ++ "*ε"
