OAI/LinearAlgebra/MatrixMultiplication/CoppersmithWinograd/CWLeafRestrictions.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Coppersmith–Winograd tensors, tensor powers and local restrictions.

  1. def OAI.MatrixMultiplication.CWLeafRestrictions.lastLabel line 12
  2. def OAI.MatrixMultiplication.CWLeafRestrictions.complement line 14
  3. theorem OAI.MatrixMultiplication.CWLeafRestrictions.complement_zero line 17
  4. theorem OAI.MatrixMultiplication.CWLeafRestrictions.complement_last line 20
  5. theorem OAI.MatrixMultiplication.CWLeafRestrictions.complement_involution line 23
  6. theorem OAI.MatrixMultiplication.CWLeafRestrictions.complement_interior line 27
  7. theorem OAI.MatrixMultiplication.CWLeafRestrictions.zero_support_iff line 35
  8. theorem OAI.MatrixMultiplication.CWLeafRestrictions.tensor_zero_matching line 70
  9. theorem OAI.MatrixMultiplication.CWLeafRestrictions.tensor_middle_zero_matching line 76
  10. theorem OAI.MatrixMultiplication.CWLeafRestrictions.tensor_last_zero_matching line 83
  11. theorem OAI.MatrixMultiplication.CWLeafRestrictions.zeroX_leaf line 90
  12. theorem OAI.MatrixMultiplication.CWLeafRestrictions.zeroY_leaf line 100
  13. theorem OAI.MatrixMultiplication.CWLeafRestrictions.zeroZ_leaf line 112