coe_mul_star_self — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem coe_mul_star_self (x : spinGroup Q) : (x : CliffordAlgebra Q) * star x = 1 :=
  mul_star_self_of_mem x.prop

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