instRing

Mathlib.Algebra.Quaternion

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

English

For any commutative ring R, the quaternion algebra ℍ(R) carries a ring structure inherited from QuaternionAlgebra.

Русский

Для коммутативного кольца R алгебра кватернионов ℍ(R) обладает структурой кольца.

LaTeX

$$$$ \mathbb{H}(R) \text{ is a ring (with the inherited operations).} $$$$

Lean4

instance instRing : Ring ℍ[R] :=
  QuaternionAlgebra.instRing

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

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

Разделы

Аффилиация

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