imK_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 k-component is zero.

Русский

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

LaTeX

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

Lean4

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

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