# mathlibdocumentation

The main result is tensor_algebra.graded_algebra, which says that the tensor algebra is a ℕ-graded algebra.

def tensor_algebra.graded_algebra.ι (R : Type u_1) (M : Type u_2) [ M] :
M →ₗ[R] (λ (i : ), ((tensor_algebra.ι R).range ^ i))

A version of tensor_algebra.ι that maps directly into the graded structure. This is primarily an auxiliary construction used to provide tensor_algebra.graded_algebra.

Equations
theorem tensor_algebra.graded_algebra.ι_apply (R : Type u_1) (M : Type u_2) [ M] (m : M) :
= (direct_sum.of (λ (i : ), ((tensor_algebra.ι R).range ^ i)) 1) m, _⟩
@[protected, instance]
def tensor_algebra.graded_algebra {R : Type u_1} {M : Type u_2} [ M] :

The tensor algebra is graded by the powers of the submodule (tensor_algebra.ι R).range.

Equations