instStarMulSubtypeCliffordAlgebraMemSubmonoid

Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

URI: https://scilib.ai/kg/mathlib#spinGroup.instStarMulSubtypeCliffordAlgebraMemSubmonoid

English

For every element x in spinGroup Q, star x equals the inverse x^{-1} in the group SpinGroup.

Русский

Для каждого x в SpinGroup(Q) звезда x равна обратному x^{-1} в группе spinGroup.

LaTeX

$$star x = x^{-1} for all x in \operatorname{spinGroup}(Q).$$

Lean4

instance : StarMul (spinGroup Q)
    where
  star_involutive _ := Subtype.ext <| star_involutive _
  star_mul _ _ := Subtype.ext <| star_mul _ _

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

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

Разделы

Аффилиация

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