Character additivity for binary tensor sums

The summands may have different finite coordinate types. A binary sum is a coordinate reindexing of the dependent direct sum over Bool.

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.Character.value_sumTensor {K : Type} [Field K] (χ : Character K) {X Y Z U V W : Type} [Fintype X] [Fintype Y] [Fintype Z] [Fintype U] [Fintype V] [Fintype W] (T : Foundation.Tensor K X Y Z) (S : Foundation.Tensor K U V W) : χ.value (sumTensor T S) = χ.value T + χ.value S

A character is additive on binary direct sums with arbitrary finite coordinate types.