OAI/LinearAlgebra/MatrixMultiplication/AuxiliarySeparation/Tensor/DirectSumClass.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite direct sums in the tensor semiring

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

  1. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_directSum_reindex line 21
  2. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_directSum_option line 30
  3. theorem OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf_directSum line 47

    Source documentation

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

    theorem classOf_directSum {ι : Type*} [Fintype ι] [dec : DecidableEq ι]
    (T : ι → Tensor ℂ X Y Z) :
    classOf (Tensor.directSum T) = ∑ i, classOf (T i) := by
…

    Mentions: OAI.MatrixMultiplication.AuxiliarySeparation.TensorSemiring.classOf