English
If a and b have coordinate representations a = (a1,a2,a3,a4) and b = (b1,b2,b3,b4), then their product is the quaternion with coordinates given by the standard coordinate multiplication formula displayed in the statement.
Русский
Если a = (a1,a2,a3,a4) и b = (b1,b2,b3,b4), то их произведение имеет координаты, заданные стандартной формулой умножения координат.
LaTeX
$$$(a_1,a_2,a_3,a_4) \cdot (b_1,b_2,b_3,b_4) = (a_1 b_1 + c_1 a_2 b_2 + c_3 a_3 b_3 + c_2 c_3 a_3 b_4 - c_1 c_3 a_4 b_4,\; a_1 b_2 + a_2 b_1 + c_2 a_2 b_2 - c_3 a_3 b_4 + c_3 a_4 b_3,\; a_1 b_3 + c_1 a_2 b_4 + a_3 b_1 + c_2 a_3 b_2 - c_1 a_4 b_2,\; a_1 b_4 + a_2 b_3 + c_2 a_2 b_4 - a_3 b_2 + a_4 b_1)$$$
Lean4
/-- Multiplication is given by
* `1 * x = x * 1 = x`;
* `i * i = c₁ + c₂ * i`;
* `j * j = c₃`;
* `i * j = k`, `j * i = c₂ * j - k`;
* `k * k = - c₁ * c₃`;
* `i * k = c₁ * j + c₂ * k`, `k * i = -c₁ * j`;
* `j * k = c₂ * c₃ - c₃ * i`, `k * j = c₃ * i`. -/
@[simps]
instance : Mul ℍ[R,c₁,c₂,c₃] :=
⟨fun a b =>
⟨a.1 * b.1 + c₁ * a.2 * b.2 + c₃ * a.3 * b.3 + c₂ * c₃ * a.3 * b.4 - c₁ * c₃ * a.4 * b.4,
a.1 * b.2 + a.2 * b.1 + c₂ * a.2 * b.2 - c₃ * a.3 * b.4 + c₃ * a.4 * b.3,
a.1 * b.3 + c₁ * a.2 * b.4 + a.3 * b.1 + c₂ * a.3 * b.2 - c₁ * a.4 * b.2,
a.1 * b.4 + a.2 * b.3 + c₂ * a.2 * b.4 - a.3 * b.2 + a.4 * b.1⟩⟩
