Q_apply — Mathlib

English

There is a real‑algebra homomorphism from CliffordAlgebra (Q c1 c2) to the quaternion algebra ℍ[R,c1,c2] giving the quaternionic realization of the Clifford algebra.

Русский

Существует реал‑алгебровый гомоморфизм от CliffordAlgebra(Q c1 c2) в quaternion algebra ℍ[R,c1,c2], реализующий клиффордову алгебру через кватернионы.

LaTeX

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

Lean4

@[simp]
theorem Q_apply (v : R × R) : Q c₁ c₂ v = c₁ * (v.1 * v.1) + c₂ * (v.2 * v.2) :=
  rfl

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