English
The quaternion algebra ℍ[R,c1,c2,c3] is equipped with a multiplication defined by the coordinate rules for 1,i,j,k, namely the listed products i^2 = c1, j^2 = c3, k^2 = -c1 c3, and the cross products i j = k, j i = c2 j - k, etc.
Русский
Алгебра кватернионов ℍ оснащена умножением, заданным координатными правилами для 1,i,j,k: i^2 = c1, j^2 = c3, k^2 = -c1 c3, i j = k, j i = c2 j - k и прочие сочетания.
LaTeX
$$$\text{Mul }\; \; \text{on } \mathbb{H}=\mathbb{H}(R,c_1,c_2,c_3)\text{ with } i^2=c_1,\ j^2=c_3,\ k^2=-c_1 c_3,\ i j = k,\ j i=c_2 j - k,\ i k = c_1 j + c_2 k,\ k i = -c_1 j,\ j k = c_2 c_3 - c_3 i,\ k j = c_3 i.$$$
Lean4
@[simp]
theorem mk_mul_mk (a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : R) :
(mk a₁ a₂ a₃ a₄ : ℍ[R,c₁,c₂,c₃]) * mk b₁ b₂ b₃ b₄ =
mk (a₁ * b₁ + c₁ * a₂ * b₂ + c₃ * a₃ * b₃ + c₂ * c₃ * a₃ * b₄ - c₁ * c₃ * a₄ * b₄)
(a₁ * b₂ + a₂ * b₁ + c₂ * a₂ * b₂ - c₃ * a₃ * b₄ + c₃ * a₄ * b₃)
(a₁ * b₃ + c₁ * a₂ * b₄ + a₃ * b₁ + c₂ * a₃ * b₂ - c₁ * a₄ * b₂)
(a₁ * b₄ + a₂ * b₃ + c₂ * a₂ * b₄ - a₃ * b₂ + a₄ * b₁) :=
rfl
