OAI/LinearAlgebra/MatrixMultiplication/Tensor/MatrixBalancing.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Finite coefficient tensors and their algebraic transformations.

  1. def OAI.MatrixMultiplication.MatrixBalancing.swapXYApproximation line 18
  2. theorem OAI.MatrixMultiplication.MatrixBalancing.swapXY_directSum line 27
  3. def OAI.MatrixMultiplication.MatrixBalancing.directSum_swapXY line 43
  4. theorem OAI.MatrixMultiplication.MatrixBalancing.matrix_swapYZ line 54
  5. theorem OAI.MatrixMultiplication.MatrixBalancing.matrix_swapXZ line 64
  6. def OAI.MatrixMultiplication.MatrixBalancing.matrixDirectSum_swapYZ line 74
  7. def OAI.MatrixMultiplication.MatrixBalancing.matrixDirectSum_swapXZ line 84
  8. def OAI.MatrixMultiplication.MatrixBalancing.matrixDirectSum_reindex line 94
  9. def OAI.MatrixMultiplication.MatrixBalancing.matrixDirectSum_product line 113
  10. def OAI.MatrixMultiplication.MatrixBalancing.matrixDirectSum_balanced line 132
  11. def OAI.MatrixMultiplication.MatrixBalancing.finiteBalanced line 149