involute — Mathlib

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⟩

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