toQuaternion_ι — Mathlib

English

There is a natural isomorphism between CliffordAlgebra(Q c1 c2) and the quaternion algebra ℍ[R,c1,0,c2] given by toQuaternion and its inverse.

Русский

Существует естественный изоморфизм между CliffordAlgebra(Q c1 c2) и кватернионной алгеброй ℍ[R,c1,0,c2], заданный отображениями toQuaternion и его обратным.

LaTeX

$$$\operatorname{toQuaternion} : \operatorname{CliffordAlgebra}(Q c_₁ c_₂) \cong_R \mathbb{H}[R,c_₁,0,c_₂]$$$

Lean4

@[simp]
theorem toQuaternion_ι (v : R × R) : toQuaternion (ι (Q c₁ c₂) v) = (⟨0, v.1, v.2, 0⟩ : ℍ[R,c₁,0,c₂]) :=
  CliffordAlgebra.lift_ι_apply _ _ v

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