English
Let R be a ring with 0 and 1. The quaternion algebra over R is isomorphic to the direct product R × R × R × R, via q ↦ (q.re, q.imI, q.imJ, q.imK) and its inverse (a,b,c,d) ↦ a + b i + c j + d k.
Русский
Пусть R — кольцо. Алгебра кватернионов над R изоморфна прямому произведению R × R × R × R; отображение q ↦ (q.re, q.imI, q.imJ, q.imK) задаёт изоморфизм, а обратное отображение (a,b,c,d) ↦ a + b i + c j + d k задаёт обратное.
LaTeX
$$$$\mathbb{H}(R) \cong R \times R \times R \times R,$$ \\ via $q \mapsto (q.re, q.imI, q.imJ, q.imK)$ and $(a,b,c,d) \mapsto a + b\,i + c\,j + d\,k.$$$
Lean4
/-- The equivalence between the quaternions over `R` and `R × R × R × R`. -/
@[simps!]
def equivProd (R : Type*) [Zero R] [One R] [Neg R] : ℍ[R] ≃ R × R × R × R :=
QuaternionAlgebra.equivProd _ _ _
