OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/InitialHash.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. def OAI.MatrixMultiplication.AllFieldInitialHash.xKeep line 18
  2. def OAI.MatrixMultiplication.AllFieldInitialHash.yKeep line 22
  3. def OAI.MatrixMultiplication.AllFieldInitialHash.zKeep line 26
  4. theorem OAI.MatrixMultiplication.AllFieldInitialHash.ambient_support line 30
  5. theorem OAI.MatrixMultiplication.AllFieldInitialHash.target_mem_ambient line 36
  6. theorem OAI.MatrixMultiplication.AllFieldInitialHash.side_survival_iff line 42
  7. theorem OAI.MatrixMultiplication.AllFieldInitialHash.isolated_of_good line 50
  8. abbrev OAI.MatrixMultiplication.AllFieldInitialHash.SelectedTargets line 69
  9. def OAI.MatrixMultiplication.AllFieldInitialHash.toTarget line 71
  10. theorem OAI.MatrixMultiplication.AllFieldInitialHash.toTarget_injective line 74
  11. theorem OAI.MatrixMultiplication.AllFieldInitialHash.selectedTargets_card line 77
  12. def OAI.MatrixMultiplication.AllFieldInitialHash.selectedExecution line 84
  13. theorem OAI.MatrixMultiplication.AllFieldInitialHash.selectedExecution_copies line 99
  14. theorem OAI.MatrixMultiplication.AllFieldInitialHash.exists_selectedExecution line 109