instStarSubtypeCliffordAlgebraMemSubmonoid

English

The spinGroup Q inherits a star operation from the ambient Clifford algebra. For every element x in spinGroup Q, the star of x is obtained by applying the ambient star on CliffordAlgebra and then reinterpreting the result as a spinGroup element; in particular star x lies in spinGroup Q.

Русский

Группа spinGroup(Q) наследует операцию звезды из окружающей алгебры клиффорд. Для любого элемента x из spinGroup(Q) звездой x является элемент, полученный применением звезды в CliffordAlgebra и последующим возвращением к элементу spinGroup; то есть star x принадлежит spinGroup Q.

LaTeX

$$$\forall x \in \operatorname{spinGroup}(Q), \ star\ x \in \operatorname{spinGroup}(Q).$$$

Lean4

instance : Star (spinGroup Q) where star x := ⟨star x, star_mem x.prop⟩

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