Documentation

Mathlib.Algebra.DualQuaternion

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 #

source
def Quaternion.dualNumberEquiv {R : Type u_1} [CommRing R] :
Quaternion (DualNumber R) ≃ₐ[R] DualNumber (Quaternion R)

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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Lemmas characterizing Quaternion.dualNumberEquiv.

    source
    @[simp]
    theorem Quaternion.re_fst_dualNumberEquiv {R : Type u_1} [CommRing R] (q : Quaternion (DualNumber R)) :
    (TrivSqZeroExt.fst (Quaternion.dualNumberEquiv q)).re = TrivSqZeroExt.fst q.re
    source
    @[simp]
    theorem Quaternion.imI_fst_dualNumberEquiv {R : Type u_1} [CommRing R] (q : Quaternion (DualNumber R)) :
    (TrivSqZeroExt.fst (Quaternion.dualNumberEquiv q)).imI = TrivSqZeroExt.fst q.imI
    source
    @[simp]
    theorem Quaternion.imJ_fst_dualNumberEquiv {R : Type u_1} [CommRing R] (q : Quaternion (DualNumber R)) :
    (TrivSqZeroExt.fst (Quaternion.dualNumberEquiv q)).imJ = TrivSqZeroExt.fst q.imJ
    source
    @[simp]
    theorem Quaternion.imK_fst_dualNumberEquiv {R : Type u_1} [CommRing R] (q : Quaternion (DualNumber R)) :
    (TrivSqZeroExt.fst (Quaternion.dualNumberEquiv q)).imK = TrivSqZeroExt.fst q.imK
    source
    @[simp]
    theorem Quaternion.re_snd_dualNumberEquiv {R : Type u_1} [CommRing R] (q : Quaternion (DualNumber R)) :
    (TrivSqZeroExt.snd (Quaternion.dualNumberEquiv q)).re = TrivSqZeroExt.snd q.re
    source
    @[simp]
    theorem Quaternion.imI_snd_dualNumberEquiv {R : Type u_1} [CommRing R] (q : Quaternion (DualNumber R)) :
    (TrivSqZeroExt.snd (Quaternion.dualNumberEquiv q)).imI = TrivSqZeroExt.snd q.imI
    source
    @[simp]
    theorem Quaternion.imJ_snd_dualNumberEquiv {R : Type u_1} [CommRing R] (q : Quaternion (DualNumber R)) :
    (TrivSqZeroExt.snd (Quaternion.dualNumberEquiv q)).imJ = TrivSqZeroExt.snd q.imJ
    source
    @[simp]
    theorem Quaternion.imK_snd_dualNumberEquiv {R : Type u_1} [CommRing R] (q : Quaternion (DualNumber R)) :
    (TrivSqZeroExt.snd (Quaternion.dualNumberEquiv q)).imK = TrivSqZeroExt.snd q.imK
    source
    @[simp]
    theorem Quaternion.fst_re_dualNumberEquiv_symm {R : Type u_1} [CommRing R] (d : DualNumber (Quaternion R)) :
    TrivSqZeroExt.fst ((AlgEquiv.symm Quaternion.dualNumberEquiv) d).re = (TrivSqZeroExt.fst d).re
    source
    @[simp]
    theorem Quaternion.fst_imI_dualNumberEquiv_symm {R : Type u_1} [CommRing R] (d : DualNumber (Quaternion R)) :
    TrivSqZeroExt.fst ((AlgEquiv.symm Quaternion.dualNumberEquiv) d).imI = (TrivSqZeroExt.fst d).imI
    source
    @[simp]
    theorem Quaternion.fst_imJ_dualNumberEquiv_symm {R : Type u_1} [CommRing R] (d : DualNumber (Quaternion R)) :
    TrivSqZeroExt.fst ((AlgEquiv.symm Quaternion.dualNumberEquiv) d).imJ = (TrivSqZeroExt.fst d).imJ
    source
    @[simp]
    theorem Quaternion.fst_imK_dualNumberEquiv_symm {R : Type u_1} [CommRing R] (d : DualNumber (Quaternion R)) :
    TrivSqZeroExt.fst ((AlgEquiv.symm Quaternion.dualNumberEquiv) d).imK = (TrivSqZeroExt.fst d).imK
    source
    @[simp]
    theorem Quaternion.snd_re_dualNumberEquiv_symm {R : Type u_1} [CommRing R] (d : DualNumber (Quaternion R)) :
    TrivSqZeroExt.snd ((AlgEquiv.symm Quaternion.dualNumberEquiv) d).re = (TrivSqZeroExt.snd d).re
    source
    @[simp]
    theorem Quaternion.snd_imI_dualNumberEquiv_symm {R : Type u_1} [CommRing R] (d : DualNumber (Quaternion R)) :
    TrivSqZeroExt.snd ((AlgEquiv.symm Quaternion.dualNumberEquiv) d).imI = (TrivSqZeroExt.snd d).imI
    source
    @[simp]
    theorem Quaternion.snd_imJ_dualNumberEquiv_symm {R : Type u_1} [CommRing R] (d : DualNumber (Quaternion R)) :
    TrivSqZeroExt.snd ((AlgEquiv.symm Quaternion.dualNumberEquiv) d).imJ = (TrivSqZeroExt.snd d).imJ
    source
    @[simp]
    theorem Quaternion.snd_imK_dualNumberEquiv_symm {R : Type u_1} [CommRing R] (d : DualNumber (Quaternion R)) :
    TrivSqZeroExt.snd ((AlgEquiv.symm Quaternion.dualNumberEquiv) d).imK = (TrivSqZeroExt.snd d).imK