coe_star_mul_self — Mathlib

English

For every element x of spinGroup Q, the product of star x with x equals the multiplicative identity in the ambient algebra, i.e., star x is a left inverse of x.

Русский

Для каждого элемента x из spinGroup(Q) произведение star x на x даёт единицу: star x является левым обратным к x.

LaTeX

$$$(\star x)\,x = 1$ in the Clifford algebra for all $x \in \operatorname{spinGroup}(Q)$.$$

Lean4

theorem coe_star_mul_self (x : spinGroup Q) : (star x : CliffordAlgebra Q) * x = 1 :=
  star_mul_self_of_mem x.prop

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