imI_ratCast — Mathlib

English

Let q be any rational number. When q is viewed as a quaternion in the quaternion algebra over R, its coefficient of the i-component is zero.

Русский

Пусть q — произвольное рациональное число. Когда q рассматривается как квадривиан над R, коэффициент при i в этом квадривиане равен нулю.

LaTeX

$$$\forall q \in \mathbb{Q}: (q \in \mathbb{H}(R))_{\mathrm{imI}} = 0$$$

Lean4

@[simp, norm_cast]
theorem imI_ratCast (q : ℚ) : (q : ℍ[R]).imI = 0 :=
  rfl

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