Results about the grading structure of the tensor algebra #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
The main result is
tensor_algebra.graded_algebra, which says that the tensor algebra is a
The tensor algebra is graded by the powers of the submodule