OAI/LinearAlgebra/MatrixMultiplication/Tensor/ComplexSeparatedTensorDecomposition.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Finite coefficient tensors and their algebraic transformations.

  1. def OAI.MatrixMultiplication.Foundation.Tensor.dependentDirectSum line 18
  2. theorem OAI.MatrixMultiplication.Foundation.Tensor.dependentDirectSum_matching line 26
  3. theorem OAI.MatrixMultiplication.Foundation.Tensor.dependentDirectSum_zero_of_left_ne line 32
  4. def OAI.MatrixMultiplication.Foundation.Tensor.directSumCoordinateEquiv line 38
  5. theorem OAI.MatrixMultiplication.Foundation.Tensor.dependentDirectSum_reindex line 49
  6. def OAI.MatrixMultiplication.Foundation.labelFiberTensor line 77
  7. def OAI.MatrixMultiplication.Foundation.fiberCoordinateEquiv line 81
  8. def OAI.MatrixMultiplication.Foundation.tagCoordinateEquiv line 93
  9. theorem OAI.MatrixMultiplication.Foundation.separatedTensor_eq_fiber_directSum line 104
  10. theorem OAI.MatrixMultiplication.Foundation.fiber_directSum_eq_separatedTensor line 134
  11. theorem OAI.MatrixMultiplication.Foundation.separatedTensor_fiber_directSum_rankAtMost line 147
  12. theorem OAI.MatrixMultiplication.Foundation.separatedTensor_fiber_directSum_rankAtMost_iff line 156
  13. theorem OAI.MatrixMultiplication.Foundation.separatedTensor_fiber_directSum_borderRankAtMost line 168
  14. theorem OAI.MatrixMultiplication.Foundation.separatedTensor_uniform_directSum_rankAtMost line 180
  15. theorem OAI.MatrixMultiplication.Foundation.separatedTensor_localModels_identity line 200
  16. theorem OAI.MatrixMultiplication.Foundation.separatedTensor_localModels_rankAtMost line 231
  17. theorem OAI.MatrixMultiplication.Foundation.separatedTensor_localModels_borderRankAtMost line 242
  18. theorem OAI.MatrixMultiplication.Foundation.separatedTensor_scalar_identity line 257
  19. theorem OAI.MatrixMultiplication.Foundation.separatedTensor_scalar_rankAtMost line 280
  20. theorem OAI.MatrixMultiplication.Foundation.separatedTensor_scalar_borderRankAtMost line 291