algebraMap_eq — Mathlib

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

Похожие утверждения