English
For v ∈ R×R, the image of ι(Q c1 c2) v under toQuaternion is the quaternion with zero real part and imaginary parts v1, v2.
Русский
Для v ∈ R×R образ ι(Q c1 c2) v при отображении toQuaternion имеет нулевую вещественную часть и мнимые части v1, v2.
LaTeX
$$$\operatorname{toQuaternion}(\iota(Q c_1 c_2)\,v) = \langle 0, v_1, v_2, 0 \rangle \in \mathbb{H}[R,c_1,0,c_2]$$$
Lean4
/-- The quaternion basis vectors within the algebra. -/
@[simps i j k]
def quaternionBasis : QuaternionAlgebra.Basis (CliffordAlgebra (Q c₁ c₂)) c₁ 0 c₂
where
i := ι (Q c₁ c₂) (1, 0)
j := ι (Q c₁ c₂) (0, 1)
k := ι (Q c₁ c₂) (1, 0) * ι (Q c₁ c₂) (0, 1)
i_mul_i := by
rw [ι_sq_scalar, Q_apply, ← Algebra.algebraMap_eq_smul_one]
simp
j_mul_j := by
rw [ι_sq_scalar, Q_apply, ← Algebra.algebraMap_eq_smul_one]
simp
i_mul_j := rfl
j_mul_i := by
rw [zero_smul, zero_sub, eq_neg_iff_add_eq_zero, ι_mul_ι_add_swap, QuadraticMap.polar]
simp
