Theorems · Definition · ring theory
Quaternion.dualNumberEquiv
{R : Type u_1} → [inst : 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.
- Defined in
- Mathlib.Algebra.DualQuaternion
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 51 from the axioms · uses propext, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- AlgEquivstatement · cited by 1,681
- Quaternionstatement and proof · cited by 206
- QuaternionAlgebra.reproof · cited by 117
- TrivSqZeroExt.fstproof · cited by 96
- QuaternionAlgebra.imIproof · cited by 91
- TrivSqZeroExt.sndproof · cited by 83
- QuaternionAlgebra.imJproof · cited by 80
- QuaternionAlgebra.imKproof · cited by 78
- DualNumberstatement and proof · cited by 52
Cited by16
Results whose statement or proof uses this declaration.
- Quaternion.imJ_fst_dualNumberEquivstatement · cited by 0
- Quaternion.re_snd_dualNumberEquivstatement · cited by 0
- Quaternion.imJ_snd_dualNumberEquivstatement · cited by 0
- Quaternion.snd_imI_dualNumberEquiv_symmstatement · cited by 0
- Quaternion.snd_imJ_dualNumberEquiv_symmstatement · cited by 0
- Quaternion.snd_imK_dualNumberEquiv_symmstatement · cited by 0
- Quaternion.snd_re_dualNumberEquiv_symmstatement · cited by 0
- Quaternion.imK_fst_dualNumberEquivstatement · cited by 0
- Quaternion.imK_snd_dualNumberEquivstatement · cited by 0
- Quaternion.fst_imI_dualNumberEquiv_symmstatement · cited by 0
- Quaternion.fst_imJ_dualNumberEquiv_symmstatement · cited by 0
- Quaternion.fst_imK_dualNumberEquiv_symmstatement · cited by 0