toClifford — Mathlib

English

There exists a canonical image of the Tensor Algebra in the Clifford Algebra, mapping TensorAlgebraι_R x to CliffordAlgebraι_Q x.

Русский

Существует каноническое отображение образа тензорной алгебры в клифордовой алгебре, переводя TensorAlgebra.ι_R x в CliffordAlgebra.ι_Q x.

LaTeX

$$$ toClifford : TensorAlgebra\;_R\; M \to_a CliffordAlgebra Q $$$

Lean4

/-- The canonical image of the `TensorAlgebra` in the `CliffordAlgebra`, which maps
`TensorAlgebra.ι R x` to `CliffordAlgebra.ι Q x`. -/
def toClifford : TensorAlgebra R M →ₐ[R] CliffordAlgebra Q :=
  TensorAlgebra.lift R (CliffordAlgebra.ι Q)

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