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