English
For a quaternion q = ⟨a1, a2, a3, a4⟩ in ℍ[R,c1,0,c2], its image under ofQuaternion has explicit coordinates in Clifford algebra: it equals algebraMap_R a1 plus a2 times the embedded i, plus a3 times the embedded j, plus a4 times the product of the two embedded generators.
Русский
Для кватерниона q = ⟨a1, a2, a3, a4⟩ из ℍ[R,c1,0,c2] образ ofQuaternion имеет явное представление в клиффордовой алгебре: равно algebraMap_R a1 + a2 ι(Q)(1,0) + a3 ι(Q)(0,1) + a4(ι(Q)(1,0)·ι(Q)(0,1)).
LaTeX
$$$\ofQuaternion(\langle a_{1},a_{2},a_{3},a_{4}\rangle) = \mathrm{algebraMap}\ R\_{\mathbb{Clifford}}(a_{1}) + a_{2} \iota(Q)(1,0) + a_{3} \iota(Q)(0,1) + a_{4} \big( \iota(Q)(1,0) \cdot \iota(Q)(0,1) \big)$$$
Lean4
@[simp]
theorem ofQuaternion_mk (a₁ a₂ a₃ a₄ : R) :
ofQuaternion (⟨a₁, a₂, a₃, a₄⟩ : ℍ[R,c₁,0,c₂]) =
algebraMap R _ a₁ + a₂ • ι (Q c₁ c₂) (1, 0) + a₃ • ι (Q c₁ c₂) (0, 1) +
a₄ • (ι (Q c₁ c₂) (1, 0) * ι (Q c₁ c₂) (0, 1)) :=
rfl
