English
A basis on M induces a basis on TensorAlgebra R M indexed by the free monoid on κ, obtained by transporting the FreeAlgebra basis along the inverse of the equivalence with the tensor algebra.
Русский
База на M порождает базис на TensorAlgebra R M, индексируемый свободным моноидом κ, полученный перенесением базы FreeAlgebra через обратное отображение эквивалентности с тензорной алгеброй.
LaTeX
$$$ (Module.Basis.tensorAlgebra b) : Basis (FreeMonoid κ) R (TensorAlgebra R M) $$$
Lean4
/-- A basis on `M` can be lifted to a basis on `TensorAlgebra R M` -/
@[simps! repr_apply]
noncomputable def _root_.Module.Basis.tensorAlgebra (b : Basis κ R M) : Basis (FreeMonoid κ) R (TensorAlgebra R M) :=
(FreeAlgebra.basisFreeMonoid R κ).map <| (equivFreeAlgebra b).symm.toLinearEquiv
