star_mul_self

Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

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

English

In pinGroup Q, star x times x equals the identity, i.e., star x is a left inverse of x in CliffordAlgebra Q.

Русский

В pinGroup Q звезда x слева является обратной к x в CliffordAlgebra Q, то есть star x · x = 1.

LaTeX

$$$(\\star x : \\mathrm{CliffordAlgebra}\\ Q) \\cdot x = 1$$$

Lean4

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

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

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

Разделы

Аффилиация

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