English
Let Q be a quadratic form on a module M over a commutative ring R. The star operation on elements of pinGroup Q corresponds, via the natural embedding into the Clifford algebra, to the Clifford algebra star operation. In particular, for any x in pinGroup Q, the image of star x in CliffordAlgebra Q equals the star of x viewed inside CliffordAlgebra Q.
Русский
Пусть Q — квадратичная форма на модуле M над коммутативной кольцом R. Операция звезды на элементах pinGroup Q совместима с операцией звезды в CliffordAlgebra Q через естественное вложение. То есть для любого x ∈ pinGroup Q образ star x в CliffordAlgebra Q равен звезде x, взятой как элемент CliffordAlgebra Q.
LaTeX
$$$\\uparrow(\\star x) = (\\star x : \\mathrm{CliffordAlgebra}\\ Q)$$$
Lean4
@[simp, norm_cast]
theorem coe_star {x : pinGroup Q} : ↑(star x) = (star x : CliffordAlgebra Q) :=
rfl
