Definition. Hamilton's Quaternions [fgap-0006]
AGENTDRAFTED
The algebra of real quaternions is the 4-dimensional real
vector space
\[
\mathbb {H}
=\mathbb {R}1\oplus \mathbb {R}i\oplus \mathbb {R}j\oplus \mathbb {R}k.
\]
Thus every quaternion can be written uniquely as
\[
q=a+bi+cj+dk,\qquad a,b,c,d\in \mathbb {R}.
\]
Addition and real scalar multiplication are coordinatewise. Multiplication is
extended bilinearly from \(1\) as the multiplicative identity and the table
\[
\begin {gathered}
i^2=j^2=k^2=ijk=-1,\\
ij=k,\quad jk=i,\quad ki=j,\\
ji=-k,\quad kj=-i,\quad ik=-j.
\end {gathered}
\]
This makes \(\mathbb {H}\) an associative, noncommutative real algebra. In
Voight's notation, \(\mathbb {H}=(-1,-1\mid \mathbb {R})\); see
[voight2021quaternion, def. 2.2.1 and ex. 2.2.3].
More generally, when \(F\) is a field of characteristic different from
\(2\) and \(a,b\in F^\times \), the symbol
\[
(a,b\mid F)
\]
denotes the quaternion algebra over \(F\) generated by elements \(i,j\) with
\[
i^2=a,\qquad j^2=b,\qquad ji=-ij.
\]
The two slots record the scalars assigned to the squares of the two
generators. With \(k=ij\), the elements \(1,i,j,k\) form an \(F\)-basis. Thus
the two entries \(-1,-1\) in
\((-1,-1\mid \mathbb {R})\) say precisely that \(i^2=-1\) and \(j^2=-1\); the
anticommutation relation then gives \(k^2=-1\).
For \(q=a+bi+cj+dk\), its quaternion conjugate and
reduced norm are
\[
\overline {q}=a-bi-cj-dk,\qquad
\operatorname {nrd}(q)=q\overline {q}
=a^2+b^2+c^2+d^2.
\]
We also have \(\overline {q}q=\operatorname {nrd}(q)\). If \(q\ne 0\), then
\(\operatorname {nrd}(q)>0\) and
\[
q^{-1}=\frac {\overline {q}}{\operatorname {nrd}(q)}.
\]
So every nonzero quaternion is invertible. This is the standard involution and
reduced norm specialized to Hamilton's Quaternions; see
[voight2021quaternion, secs. 3.1--3.3].
The corresponding Mathlib type is Quaternion.