Graded vector space

Direct sum of graded vector spaces

The direct sum of -graded vector spaces is the direct sum of vector spaces #m/def/linalg

with the gradation where

for .

#state/tidy| #lang/en | #SemBr