mul_star_self — Mathlib

English

The spinGroup Q forms a group with the inverse operation given by star, so the star maps are group inverses within spinGroup.

Русский

Группа spinGroup(Q) образует группу, где обратное к элементу задается через star.

LaTeX

$$There is a group structure on \operatorname{spinGroup}(Q) with inverse given by star, i.e., x^{-1} = star x.$$

Lean4

@[simp]
theorem mul_star_self (x : spinGroup Q) : x * star x = 1 :=
  Subtype.ext <| coe_mul_star_self x

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