OAI/LinearAlgebra/MatrixFields/Tensors/ComplexSeparatedTensorDecomposition.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.dependentDirectSum line 18
  2. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.dependentDirectSum_matching line 26
  3. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.dependentDirectSum_zero_of_left_ne line 32
  4. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.directSumCoordinateEquiv line 38
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.Tensor.dependentDirectSum_reindex line 49
  6. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.labelFiberTensor line 74
  7. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.fiberCoordinateEquiv line 78
  8. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.tagCoordinateEquiv line 90
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.separatedTensor_eq_fiber_directSum line 101
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.fiber_directSum_eq_separatedTensor line 131
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.separatedTensor_fiber_directSum_rankAtMost line 144
  12. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.separatedTensor_fiber_directSum_rankAtMost_iff line 153
  13. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.separatedTensor_fiber_directSum_borderRankAtMost line 165
  14. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.separatedTensor_uniform_directSum_rankAtMost line 177
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.separatedTensor_localModels_identity line 197
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.separatedTensor_localModels_rankAtMost line 228
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.separatedTensor_localModels_borderRankAtMost line 239
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.separatedTensor_scalar_identity line 254
  19. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.separatedTensor_scalar_rankAtMost line 277
  20. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.separatedTensor_scalar_borderRankAtMost line 288