OAI/LinearAlgebra/MatrixMultiplication/CoppersmithWinograd/CWZeroGeometry.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Coppersmith–Winograd tensors, tensor powers and local restrictions.

  1. def OAI.MatrixMultiplication.CWZeroGeometry.zeroAxis line 12
  2. def OAI.MatrixMultiplication.CWZeroGeometry.maxAxis line 15
  3. theorem OAI.MatrixMultiplication.CWZeroGeometry.zeroAxis_spec line 18
  4. theorem OAI.MatrixMultiplication.CWZeroGeometry.maxAxis_spec line 26
  5. theorem OAI.MatrixMultiplication.CWZeroGeometry.shapeMax_le_total line 44
  6. theorem OAI.MatrixMultiplication.CWZeroGeometry.shapeMax_pos line 48
  7. theorem OAI.MatrixMultiplication.CWZeroGeometry.zero_ne_selected line 55
  8. theorem OAI.MatrixMultiplication.CWZeroGeometry.max_add_complement line 63
  9. theorem OAI.MatrixMultiplication.CWZeroGeometry.eq_placedShape line 67
  10. theorem OAI.MatrixMultiplication.CWZeroGeometry.physicalShape_eq_placedShape line 76
  11. theorem OAI.MatrixMultiplication.CWZeroGeometry.selected_add_remaining line 88