star_mul_self

Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

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

English

In spinGroup Q, star x is the inverse of x, i.e., star x equals x^{-1} in the ambient group structure.

Русский

В spinGroup(Q) звездaя операция совпадает с обращением: star x = x^{-1}.

LaTeX

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

Lean4

@[simp]
theorem star_mul_self (x : spinGroup Q) : star x * x = 1 :=
  Subtype.ext <| coe_star_mul_self x

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

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

Разделы

Аффилиация

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