OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/ConstructionData.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. structure OAI.MatrixMultiplication.AllFieldConstructionData.Data line 20
  2. abbrev OAI.MatrixMultiplication.AllFieldConstructionData.Tags line 29
  3. instance OAI.MatrixMultiplication.AllFieldConstructionData.tagsFintype line 33
  4. def OAI.MatrixMultiplication.AllFieldConstructionData.execution line 36
  5. theorem OAI.MatrixMultiplication.AllFieldConstructionData.card_tags line 45
  6. theorem OAI.MatrixMultiplication.AllFieldConstructionData.execution_copies line 58
  7. theorem OAI.MatrixMultiplication.AllFieldConstructionData.tags_pos line 68
  8. def OAI.MatrixMultiplication.AllFieldConstructionData.witness line 79
  9. theorem OAI.MatrixMultiplication.AllFieldConstructionData.witness_volume line 89
  10. theorem OAI.MatrixMultiplication.AllFieldConstructionData.witness_multiplicity line 99
  11. theorem OAI.MatrixMultiplication.AllFieldConstructionData.witness_rankBound line 111