instStar

Mathlib.Algebra.Quaternion

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

English

There is a star operation on ℍ(R) given by QuaternionAlgebra.instStarQuaternionAlgebra, giving a conjugation-like involution.

Русский

Для ℍ(R) задано звездообразование (инволюция), задаваемое QuaternionAlgebra.instStarQuaternionAlgebra.

LaTeX

$$$$ \ast:\mathbb{H}(R) \to \mathbb{H}(R) \quad \text{involution (Star).} $$$$

Lean4

instance : Star ℍ[R] :=
  QuaternionAlgebra.instStarQuaternionAlgebra

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

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

Разделы

Аффилиация

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