English
There is a natural algebra structure on the quaternion algebra over S whenever S → R is an algebra: the quaternion algebra becomes an S-algebra compatible with the given algebra maps.
Русский
Существует естественная структура алгебры над S на кватернионной алгебре, если S→R образует алгебру: кватернионная алгебра становится S-алгеброй, совместимой с данными отображениями базового кольца.
LaTeX
$$$\mathbb{H}(R;c_1,c_2,c_3) \text{ carries an } S\text{-algebra structure compatible with } S \to R.$$$
Lean4
/-- `QuaternionAlgebra.re` as a `LinearMap` -/
@[simps]
def reₗ : ℍ[R,c₁,c₂,c₃] →ₗ[R] R where
toFun := re
map_add' _ _ := rfl
map_smul' _ _ := rfl
