toTensorAlgebra — Mathlib

English

There is a canonical embedding from the nth tensor power of M into TensorAlgebra R M.

Русский

Существует каноническое вложение из n-й тензорной степени M в TensorAlgebra R M.

LaTeX

$$$ toTensorAlgebra : ⨂[R]^n M \rightarrowₗ[R] TensorAlgebra R M $$$

Lean4

/-- The canonical embedding from a tensor power to the tensor algebra -/
def toTensorAlgebra {n} : ⨂[R]^n M →ₗ[R] TensorAlgebra R M :=
  PiTensorProduct.lift (TensorAlgebra.tprod R M n)

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