English
The inclusion of spinGroup Q into CliffordAlgebra Q commutes with the star operation; i.e., the star of the image of x equals the image of the star of x.
Русский
Включение spinGroup(Q) в CliffordAlgebra(Q) коммутирует с операцией звезды: образ star x совпадает с звездой образа x.
LaTeX
$$$\uparrow(\operatorname{star}(x)) = \operatorname{star}(\uparrow(x))$ for all $x \in \operatorname{spinGroup}(Q)$.$$
Lean4
@[simp, norm_cast]
theorem coe_star {x : spinGroup Q} : ↑(star x) = (star x : CliffordAlgebra Q) :=
rfl