OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/Source.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. abbrev OAI.MatrixMultiplication.AllFieldSource.Word line 17
  2. abbrev OAI.MatrixMultiplication.AllFieldSource.Index line 19
  3. def OAI.MatrixMultiplication.AllFieldSource.tensor line 21
  4. def OAI.MatrixMultiplication.AllFieldSource.rankBudget line 25
  5. theorem OAI.MatrixMultiplication.AllFieldSource.rank_bound line 28
  6. theorem OAI.MatrixMultiplication.AllFieldSource.rankBudget_pos line 38
  7. theorem OAI.MatrixMultiplication.AllFieldSource.rankBudget_prod line 44
  8. def OAI.MatrixMultiplication.AllFieldSource.matrixTarget line 49
  9. theorem OAI.MatrixMultiplication.AllFieldSource.restricted_rank_bound line 58
  10. def OAI.MatrixMultiplication.AllFieldSource.restrictedApproximation line 70
  11. def OAI.MatrixMultiplication.AllFieldSource.ofRestriction line 79
  12. theorem OAI.MatrixMultiplication.AllFieldSource.ofRestriction_polynomial line 101