English
Grade involution defines an algebra automorphism involute of CliffordAlgebra Q, sending each generator ι_Q(m) to -ι_Q(m) and extending multiplicatively.
Русский
Градационная инволюция задаёт алгебраический автоморфизм involute для CliffordAlgebra Q, отправляющий каждый генератор ι_Q(m) в -ι_Q(m) и продолжая по умножению.
LaTeX
$$$ \mathrm{involute} \in \mathrm{Aut}_{R}(\mathrm{CliffordAlgebra}(Q)) \; \text{ и } \forall m:\; \mathrm{involute}(\iota_Q(m)) = -\iota_Q(m). $$$
Lean4
/-- Grade involution, inverting the sign of each basis vector. -/
def involute : CliffordAlgebra Q →ₐ[R] CliffordAlgebra Q :=
CliffordAlgebra.lift Q ⟨-ι Q, fun m => by simp⟩