star_eq_inv — Mathlib

English

Each element of spinGroup Q yields a unit in CliffordAlgebra Q, providing a natural embedding of spinGroup into the unit group of the Clifford algebra.

Русский

Каждый элемент spinGroup(Q) дает единицу в CliffordAlgebra(Q), образуя естественное вложение spinGroup в группу единиц CliffordAlgebra.

LaTeX

$$toUnits : \operatorname{spinGroup}(Q) \to (\mathrm{CliffordAlgebra}(Q))^{\times} is a monoid homomorphism.$$

Lean4

theorem star_eq_inv (x : spinGroup Q) : star x = x⁻¹ :=
  rfl

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