tprod — Mathlib

English

Given a basis b of M with index set κ, there is an R-algebra isomorphism between TensorAlgebra R M and FreeAlgebra R κ.

Русский

С учетом базиса b множества M с индексами κ существует изоморфизм R-алгебр между TensorAlgebra_R M и FreeAlgebra_R κ.

LaTeX

$$$\\exists b: \\text{Basis } κ\\, R\\, M,\\, \\mathrm{TensorAlgebra}_R M \\cong_R \\mathrm{FreeAlgebra}_R κ$$$

Lean4

/-- Construct a product of `n` elements of the module within the tensor algebra.

See also `PiTensorProduct.tprod`. -/
def tprod (n : ℕ) : MultilinearMap R (fun _ : Fin n => M) (TensorAlgebra R M) :=
  (MultilinearMap.mkPiAlgebraFin R n (TensorAlgebra R M)).compLinearMap fun _ => ι R

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