English
The toQuaternion map is compatible with the Clifford conjugation (reverse) and quaternion conjugation: star commuting with toQuaternion.
Русский
Отображение toQuaternion совместимо с клиффордовым сопряжением и коньюгированием кватернионной алгебры: сопряжение сохраняется через toQuaternion.
LaTeX
$$$\operatorname{toQuaternion}(\operatorname{star} c) = \operatorname{star}(\operatorname{toQuaternion} c)$$$
Lean4
/-- The "clifford conjugate" maps to the quaternion conjugate. -/
theorem toQuaternion_star (c : CliffordAlgebra (Q c₁ c₂)) : toQuaternion (star c) = star (toQuaternion c) :=
by
simp only [CliffordAlgebra.star_def']
induction c using CliffordAlgebra.induction with
| algebraMap r => simp
| ι x => simp
| mul x₁ x₂ hx₁ hx₂ => simp [hx₁, hx₂]
| add x₁ x₂ hx₁ hx₂ => simp [hx₁, hx₂]