toQuaternion_star — Mathlib

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₂]

Похожие утверждения