OAI/LinearAlgebra/MatrixMultiplication/CoppersmithWinograd/CWOrientedZero.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Coppersmith–Winograd tensors, tensor powers and local restrictions.

  1. theorem OAI.MatrixMultiplication.CWOrientedZero.tensor_swapXY line 16
  2. theorem OAI.MatrixMultiplication.CWOrientedZero.tensor_swapYZ line 22
  3. theorem OAI.MatrixMultiplication.CWOrientedZero.tensor_swapXZ line 27
  4. theorem OAI.MatrixMultiplication.CWOrientedZero.shape_swapXY line 31
  5. theorem OAI.MatrixMultiplication.CWOrientedZero.shape_swapYZ line 44
  6. theorem OAI.MatrixMultiplication.CWOrientedZero.shape_swapXZ line 57
  7. def OAI.MatrixMultiplication.CWOrientedZero.placedShape line 62
  8. def OAI.MatrixMultiplication.CWOrientedZero.sideWord line 65
  9. def OAI.MatrixMultiplication.CWOrientedZero.matched line 69
  10. theorem OAI.MatrixMultiplication.CWOrientedZero.local_coefficient line 72
  11. def OAI.MatrixMultiplication.CWOrientedZero.Row line 104
  12. def OAI.MatrixMultiplication.CWOrientedZero.Middle line 105
  13. def OAI.MatrixMultiplication.CWOrientedZero.Column line 106
  14. instance OAI.MatrixMultiplication.CWOrientedZero.(instance at line 107) line 107
  15. instance OAI.MatrixMultiplication.CWOrientedZero.(instance at line 109) line 109
  16. instance OAI.MatrixMultiplication.CWOrientedZero.(instance at line 111) line 111
  17. theorem OAI.MatrixMultiplication.CWOrientedZero.volume line 114
  18. theorem OAI.MatrixMultiplication.CWOrientedZero.matching_nonempty line 139
  19. def OAI.MatrixMultiplication.CWOrientedZero.ofMatching line 181
  20. theorem OAI.MatrixMultiplication.CWOrientedZero.power_coefficient line 188