OAI/LinearAlgebra/MatrixMultiplication/CoppersmithWinograd/CWWordDimensions.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Coppersmith–Winograd tensors, tensor powers and local restrictions.

  1. def OAI.MatrixMultiplication.CWWordDimensions.sitePolynomial line 19
  2. theorem OAI.MatrixMultiplication.CWWordDimensions.site_enumerator line 21
  3. theorem OAI.MatrixMultiplication.CWWordDimensions.word_enumerator line 27
  4. abbrev OAI.MatrixMultiplication.CWWordDimensions.WeightWords line 46
  5. theorem OAI.MatrixMultiplication.CWWordDimensions.card_weightWords line 48
  6. def OAI.MatrixMultiplication.CWWordDimensions.recursiveCoeff line 54
  7. theorem OAI.MatrixMultiplication.CWWordDimensions.coeff_eq_recursive line 60
  8. theorem OAI.MatrixMultiplication.CWWordDimensions.card_weightWords_fin line 74