English
The toQuaternion map respects the quaternion conjugation (star) operation: toQuaternion(star c) = star(toQuaternion c).
Русский
Отображение toQuaternion сохраняет операцию коньюгирования: toQuaternion(звезда c) = звезда(toQuaternion c).
LaTeX
$$$\operatorname{toQuaternion}(\operatorname{star} c) = \operatorname{star}(\operatorname{toQuaternion} c)$$$
Lean4
/-- Intermediate result of `CliffordAlgebraQuaternion.equiv`: clifford algebras over
`CliffordAlgebraQuaternion.Q` can be converted to `ℍ[R,c₁,c₂]`. -/
def toQuaternion : CliffordAlgebra (Q c₁ c₂) →ₐ[R] ℍ[R,c₁,0,c₂] :=
CliffordAlgebra.lift (Q c₁ c₂)
⟨{ toFun := fun v => (⟨0, v.1, v.2, 0⟩ : ℍ[R,c₁,0,c₂])
map_add' := fun v₁ v₂ => by simp
map_smul' := fun r v => by dsimp; rw [mul_zero] }, fun v =>
by
dsimp
ext
all_goals dsimp; ring⟩
