ofQuaternion_star — Mathlib

English

The map ofQuaternion preserves the quaternion conjugation with respect to the Clifford conjugation; i.e., the image of the quaternion star is the star of the image.

Русский

Отображение ofQuaternion сохраняет конъугацию кватерниона относительно конъугации Клиффорда: образ кватерниона при звездочке переходит в звездочку образа.

LaTeX

$$$\ofQuaternion(\star q) = \star(\ofQuaternion(q))$$$

Lean4

/-- The quaternion conjugate maps to the "clifford conjugate" (aka `star`). -/
@[simp]
theorem ofQuaternion_star (q : ℍ[R,c₁,0,c₂]) : ofQuaternion (star q) = star (ofQuaternion q) :=
  CliffordAlgebraQuaternion.equiv.injective <| by
    rw [equiv_apply, equiv_apply, toQuaternion_star, toQuaternion_ofQuaternion, toQuaternion_ofQuaternion]

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