Tensor algebras as direct sums of tensor powers #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
In this file we show that
tensor_algebra R M is isomorphic to a direct sum of tensor powers, as
The canonical embedding from a tensor power to the tensor algebra
The canonical map from a direct sum of tensor powers to the tensor algebra.
The canonical map from the tensor algebra to a direct sum of tensor powers.
The product of tensor products made of a single vector is the same as a single product of
all the vectors.
The tensor algebra is isomorphic to a direct sum of tensor powers.