Finite direct sums in the tensor semiring

The tensor class of a block direct sum is the sum of its constituent classes.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_directSum {K : Type} [Field K] {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Fintype X] [Fintype Y] [Fintype Z] {ι : Type u_4} [Fintype ι] [dec : DecidableEq ι] (T : ι → Foundation.Tensor K X Y Z) : classOf (Foundation.Tensor.directSum T) = ∑ i : ι, classOf (T i)

Passing to tensor classes converts every finite block direct sum to a sum.