OAI/LinearAlgebra/MatrixMultiplication/CoppersmithWinograd/CWShapePhysicalPermutation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Coppersmith–Winograd tensors, tensor powers and local restrictions.

  1. theorem OAI.MatrixMultiplication.CWShapePhysicalPermutation.tensor_swapXY line 17
  2. theorem OAI.MatrixMultiplication.CWShapePhysicalPermutation.tensor_swapYZ line 23
  3. theorem OAI.MatrixMultiplication.CWShapePhysicalPermutation.tensor_swapXZ line 28
  4. theorem OAI.MatrixMultiplication.CWShapePhysicalPermutation.tensor_permute line 32
  5. theorem OAI.MatrixMultiplication.CWShapePhysicalPermutation.strand_permute line 50
  6. theorem OAI.MatrixMultiplication.CWShapePhysicalPermutation.shapeTensor_permute line 58
  7. theorem OAI.MatrixMultiplication.CWShapePhysicalPermutation.shapeTensor_prod_permute line 79
  8. theorem OAI.MatrixMultiplication.CWShapePhysicalPermutation.shapeTensor_prod_permute_ne_zero_iff line 90
  9. theorem OAI.MatrixMultiplication.CWShapePhysicalPermutation.sidePermutation_shapeTensor line 99