coe_nnratCast — Mathlib

English

For nonnegative rational numbers, their natural embedding into the quaternion algebra coincides with the quaternion that has only a real part equal to that number.

Русский

Для чисел типа рационального неотрицательного знака их естественное вложение в кватернионную алгебру совпадает с кватернионом, у которого единственная ненулевая часть — это число.

LaTeX

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

Lean4

@[norm_cast]
theorem coe_nnratCast (q : ℚ≥0) : ↑(q : R) = (q : ℍ[R]) :=
  rfl

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