reverse — Mathlib

English

Grade reversion is a linear map sending a product to its reverse; it is the canonical anti-automorphism of CliffordAlgebra Q.

Русский

Градационная реконструкция — линейное отображение, обращающее порядок умножения; это каноническая антиавтоморфизм клиффордовой алгебры.

LaTeX

$$$ \mathrm{reverse} : \mathrm{CliffordAlgebra}(Q) \to_{R} \mathrm{CliffordAlgebra}(Q). $$$

Lean4

/-- Grade reversion, inverting the multiplication order of basis vectors.
Also called *transpose* in some literature. -/
def reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q :=
  (opLinearEquiv R).symm.toLinearMap.comp reverseOp.toLinearMap

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