English
For the spin group associated with Q on CliffordAlgebra, star preserves membership: an element x lies in spinGroup Q if and only if its star is in spinGroup Q.
Русский
Для группы spin, связанной с Q на CliffordAlgebra, звездочка сохраняет принадлежность: элемент x находится в spinGroup Q тогда и только тогда, когда star x принадлежит spinGroup Q.
LaTeX
$$$ star\\ x \\in \\operatorname{spinGroup}(Q) \\iff x \\in \\operatorname{spinGroup}(Q) $$$
Lean4
/-- An element is in `spinGroup Q` if and only if `star x` is in `spinGroup Q`.
See `star_mem` for only one direction.
-/
@[simp]
theorem star_mem_iff {x : CliffordAlgebra Q} : star x ∈ spinGroup Q ↔ x ∈ spinGroup Q :=
by
refine ⟨?_, star_mem⟩
intro hx
convert star_mem hx
exact (star_star x).symm
