OAI/LinearAlgebra/MatrixMultiplication/CoppersmithWinograd/CWStrands.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Coppersmith–Winograd tensors, tensor powers and local restrictions.

  1. theorem OAI.MatrixMultiplication.CWStrands.site_weight_zero_support line 16
  2. theorem OAI.MatrixMultiplication.CWStrands.site_weight_support line 32
  3. def OAI.MatrixMultiplication.CWStrands.weight line 47
  4. def OAI.MatrixMultiplication.CWStrands.strand line 50
  5. theorem OAI.MatrixMultiplication.CWStrands.strand_support line 53
  6. def OAI.MatrixMultiplication.CWStrands.shapeTensor line 66
  7. theorem OAI.MatrixMultiplication.CWStrands.shapeTensor_support line 71
  8. theorem OAI.MatrixMultiplication.CWStrands.weight_sum_elim line 79
  9. theorem OAI.MatrixMultiplication.CWStrands.strand_sum_elim line 84
  10. theorem OAI.MatrixMultiplication.CWStrands.shape_split line 92
  11. theorem OAI.MatrixMultiplication.CWStrands.shape_split_sub line 112
  12. def OAI.MatrixMultiplication.CWStrands.splitMatrix line 126
  13. theorem OAI.MatrixMultiplication.CWStrands.shape_split_restrict line 131