star_mul_self_of_mem

Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

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

English

If an element belongs to spinGroup Q, then its star also belongs to spinGroup Q.

Русский

Если элемент принадлежит spinGroup Q, то его звезда также принадлежит spinGroup Q.

LaTeX

$$star_mem {x : CliffordAlgebra Q} (hx : x ∈ spinGroup Q) : star x ∈ spinGroup Q$$

Lean4

@[simp]
theorem star_mul_self_of_mem {x : CliffordAlgebra Q} (hx : x ∈ spinGroup Q) : star x * x = 1 :=
  hx.1.2.1

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

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

Разделы

Аффилиация

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