English
For a commutative ring R and parameters c1,c2,c3 in R, the quaternion algebra ℍ[R,c1,c2,c3] forms a ring with the usual addition and multiplication, i.e., it satisfies the ring axioms under the quaternion multiplication rule.
Русский
Для коммутативного кольца R и параметров c1,c2,c3 ∈ R кватернионовая алгебра ℍ[R,c1,c2,c3] образует кольцо с обычным сложением и умножением; выполняются аксиомы кольца относительно умножения кватернионов.
LaTeX
$$$\mathbb{H}(R;c_1,c_2,c_3) \text{ is a ring with the standard operations.}$$$
Lean4
instance instRing : Ring ℍ[R,c₁,c₂,c₃]
where
__ := inferInstanceAs (AddCommGroupWithOne ℍ[R,c₁,c₂,c₃])
left_distrib _ _ _ := by ext <;> simp <;> ring
right_distrib _ _ _ := by ext <;> simp <;> ring
zero_mul _ := by ext <;> simp
mul_zero _ := by ext <;> simp
mul_assoc _ _ _ := by ext <;> simp <;> ring
one_mul _ := by ext <;> simp
mul_one _ := by ext <;> simp
