reverseEquiv — Mathlib

English

There is a linear equivalence of Clifford algebras given by reverse, i.e. reverse provides an automorphism a ↦ reverse(a) with an inverse given by reverse itself.

Русский

Существует линейное эквивалентное отображение клиффордовой алгебры, заданное reverse; обратное к нему тоже reverse.

LaTeX

$$$ reverseEquiv : CliffordAlgebra Q \simeq_R CliffordAlgebra Q $$$

Lean4

/-- `CliffordAlgebra.reverse` as a `LinearEquiv`. -/
@[simps!]
def reverseEquiv : CliffordAlgebra Q ≃ₗ[R] CliffordAlgebra Q :=
  LinearEquiv.ofInvolutive reverse reverse_involutive

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