instStarRing

Mathlib.Algebra.Quaternion

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

English

ℍ(R) forms a StarRing, i.e., it is a ring with a compatible star operation.

Русский

ℍ(R) образует StarRing — кольцо с совместной звездой.

LaTeX

$$$$ \text{StarRing } \mathbb{H}(R). $$$$

Lean4

instance : StarRing ℍ[R] :=
  QuaternionAlgebra.instStarRing

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

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

Разделы

Аффилиация

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