coe_ratCast — Mathlib

English

For any rational q, the quaternion embedding of q agrees with the quaternion whose real part is q and whose imaginary parts are zero.

Русский

Для любого рационального q вложение q в кватернионы согласуется с кватернионом, у которого вещественная часть равна q, а мнимые равны нулю.

LaTeX

$$$\forall q \in \mathbb{Q}: \uparrow (q : \mathbb{R}) = (q : \mathbb{H}(R))$$$

Lean4

@[norm_cast]
theorem coe_ratCast (q : ℚ) : ↑(q : R) = (q : ℍ[R]) :=
  rfl

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