OAI/LinearAlgebra/MatrixMultiplication/CoppersmithWinograd/CWCompatibilityTransfer.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Coppersmith–Winograd tensors, tensor powers and local restrictions.

  1. def OAI.MatrixMultiplication.CWCompatibilityTransfer.wordWeight line 15
  2. def OAI.MatrixMultiplication.CWCompatibilityTransfer.wordComplement line 17
  3. theorem OAI.MatrixMultiplication.CWCompatibilityTransfer.wordComplement_involution line 20
  4. theorem OAI.MatrixMultiplication.CWCompatibilityTransfer.weight_eq_zero_iff line 25
  5. theorem OAI.MatrixMultiplication.CWCompatibilityTransfer.wordWeight_zero line 28
  6. theorem OAI.MatrixMultiplication.CWCompatibilityTransfer.site_nonzero line 38
  7. theorem OAI.MatrixMultiplication.CWCompatibilityTransfer.zeroX_word_match line 46
  8. theorem OAI.MatrixMultiplication.CWCompatibilityTransfer.zeroY_word_match line 64
  9. theorem OAI.MatrixMultiplication.CWCompatibilityTransfer.zeroZ_word_match line 82
  10. theorem OAI.MatrixMultiplication.CWCompatibilityTransfer.transfer_window line 100