BinaryCharacter.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

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

theorem OAI.MatrixMultiplication.AuxiliarySeparation.Character.value_sumTensor line 22
Source documentation
A character is additive on binary direct sums with arbitrary finite coordinate types.
```
theorem value_sumTensor (χ : Character)
    {X Y Z U V W : Type}
    [Fintype X] [Fintype Y] [Fintype Z]
    [Fintype U] [Fintype V] [Fintype W]
    (T : Tensor ℂ X Y Z) (S : Tensor ℂ U V W) :
    χ.value (sumTensor T S) = χ.value T + χ.value S := by
…
```
Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.Character, OAI.MatrixMultiplication.AuxiliarySeparation.sumTensor