coe — Mathlib

English

There is a canonical embedding of R into the quaternion algebra ℍ(R) sending r to the quaternion with real part r and zero imaginary parts.

Русский

Существует каноническое вложение R в ℍ(R), отправляющее r в кватернион с вещественной частью r и нулевой мнимой частью.

LaTeX

$$$$ \iota: R \to \mathbb{H}(R), \quad \iota(r) = r \in \mathbb{H}(R). $$$$

Lean4

/-- Coercion `R → ℍ[R]`. -/
@[coe]
def coe : R → ℍ[R] :=
  QuaternionAlgebra.coe

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