English
Let R be a commutative ring and let H = ℍ[R] be the quaternion algebra over R. Via the natural embedding of R into H, each x ∈ R is identified with a quaternion whose real part is x and whose imaginary parts are all zero. Then for all x ∈ R, the real part of the embedded element is x.
Русский
Пусть R — коммутативное кольцо, H = ℍ[R] — алгебра Гамильтона над R. Встроением R в H каждое x ∈ R рассматривается как кватернион с действительной частью x и нулевыми мнимыми частями. Тогда для всякого x ∈ R действительная часть встроенного элемента равна x.
LaTeX
$$$$\forall x \in R:\ \operatorname{Re}(\iota(x)) = x.$$$$
Lean4
@[simp, norm_cast]
theorem re_coe : (x : ℍ[R]).re = x :=
rfl
