star_mul_self_of_mem

Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

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

English

An element lies in pinGroup iff its star is in pinGroup.

Русский

Элемент лежит в pinGroup тогда и только тогда, когда его звёздочка лежит в pinGroup.

LaTeX

$$$$\\text{star\_mem\_iff}:\\star x \\in \\mathrm{pinGroup}(Q) \\iff x \\in \\mathrm{pinGroup}(Q)$$$$

Lean4

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

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

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

Разделы

Аффилиация

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