mathlib3 documentation

linear_algebra.tensor_algebra.to_tensor_power

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 tensor_algebra.equiv_direct_sum.

The canonical embedding from a tensor power to the tensor algebra

Equations

The canonical map from a direct sum of tensor powers to the tensor algebra.

Equations

The canonical map from the tensor algebra to a direct sum of tensor powers.

Equations
@[simp]
@[simp]
theorem tensor_algebra.mk_reindex_cast {R : Type u_1} {M : Type u_2} [comm_semiring R] [add_comm_monoid M] [module R M] {n m : } (h : n = m) (x : tensor_power R n M) :
@[simp]

The product of tensor products made of a single vector is the same as a single product of all the vectors.