English
The real part of the left coordinate is preserved under dual-number equivalence.
Русский
Действие двойного числа сохраняет вещественную часть левого координата.
LaTeX
$$$(dualNumberEquiv q).fst.re = q.re.fst$$$
Lean4
/-- The dual quaternions can be equivalently represented as a quaternion with dual coefficients,
or as a dual number with quaternion coefficients.
See also `Matrix.dualNumberEquiv` for a similar result. -/
def dualNumberEquiv : Quaternion (DualNumber R) ≃ₐ[R] DualNumber (Quaternion R)
where
toFun q := (⟨q.re.fst, q.imI.fst, q.imJ.fst, q.imK.fst⟩, ⟨q.re.snd, q.imI.snd, q.imJ.snd, q.imK.snd⟩)
invFun d := ⟨(d.fst.re, d.snd.re), (d.fst.imI, d.snd.imI), (d.fst.imJ, d.snd.imJ), (d.fst.imK, d.snd.imK)⟩
map_mul' := by
intros
ext : 1
· rfl
· dsimp
congr 1 <;> simp <;> ring
map_add' := by
intros
rfl
commutes' _ := rfl
