Direct sum of graded vector spaces

The direct sum of $𝑆$ -graded vector spaces $(𝑉 𝑖) 𝑖 \in 𝐼$ is the direct sum of vector spaces #m/def/linalg

𝑋 = ⨁ 𝑖 \in 𝐼 𝑉 𝑖

with the gradation $𝑋 = ⨁ 𝛼 \in 𝑆 𝑋 𝛼$ where

𝑋 𝛼 = ⨁ 𝑖 \in 𝐼 𝑉 𝑖 𝛼

for $𝛼 \in 𝑆$ .

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