instCoeTC

Mathlib.Algebra.Quaternion

URI: https://scilib.ai/kg/mathlib#Quaternion.instCoeTC

English

There is a canonical CoeTC structure from R to ℍ(R), i.e., a natural way to view R as a subobject of the quaternions.

Русский

Существует каноническая структура CoeTC от R к ℍ(R), то есть естественное включение R в кватернионы.

LaTeX

$$$$ \text{There is a canonical } \mathrm{CoeTC}: R \to \mathbb{H}(R). $$$$

Lean4

instance : CoeTC R ℍ[R] :=
  ⟨coe⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru