English
The algebra map from R to the quaternion algebra sends a real element r to the quaternion with real part r and zero imaginary parts: algebraMap_R_to_H(r) = ⟨r,0,0,0⟩.
Русский
Алгебраическое отображение из R в ℍ отправляет элемент r в кватернион с вещественной частью r и нулевыми мнимыми частями: algebraMap_R_to_H(r) = ⟨r,0,0,0⟩.
LaTeX
$$$\operatorname{algebraMap}_{R \to \mathbb{H}(R;c_1,c_2,c_3)}(r) = \langle r,0,0,0\rangle.$$$
Lean4
theorem algebraMap_eq (r : R) : algebraMap R ℍ[R,c₁,c₂,c₃] r = ⟨r, 0, 0, 0⟩ :=
rfl