instGroupSubtypeCliffordAlgebraMemSubmonoid

English

The star operation is compatible with multiplication in spinGroup Q, i.e., the star map is a StarMul on spinGroup.

Русский

Операция звезды совместима с умножением в spinGroup(Q); звезда образует структуру StarMul на spinGroup.

LaTeX

$$starMul on \operatorname{spinGroup}(Q) is defined by star(ab) = star(b) star(a).$$

Lean4

/-- `spinGroup Q` forms a group where the inverse is `star`. -/
instance : Group (spinGroup Q) where
  inv := star
  inv_mul_cancel := star_mul_self

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