reverseOpEquiv — Mathlib

English

`reverseOpEquiv` is an algebra equivalence between CliffordAlgebra Q and its opposite.

Русский

`reverseOpEquiv` — алгебраическое эквивалентное отображение между CliffordAlgebra Q и её противоположной алгеброй.

LaTeX

$$$ \text{reverseOpEquiv} : \mathrm{CliffordAlgebra}(Q) \simeq_{R} (\mathrm{CliffordAlgebra}(Q))^{\mathrm{op}}. $$$

Lean4

/-- `CliffordAlgebra.reverseEquiv` as an `AlgEquiv` to the opposite algebra -/
@[simps! apply]
def reverseOpEquiv : CliffordAlgebra Q ≃ₐ[R] (CliffordAlgebra Q)ᵐᵒᵖ :=
  AlgEquiv.ofAlgHom reverseOp (AlgHom.opComm reverseOp)
    (AlgHom.unop.injective <| hom_ext <| LinearMap.ext fun _ => by simp) (hom_ext <| LinearMap.ext fun _ => by simp)

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