OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/ZeroWords.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. def OAI.MatrixMultiplication.AllFieldZeroWords.length line 17
  2. def OAI.MatrixMultiplication.AllFieldZeroWords.shape line 18
  3. def OAI.MatrixMultiplication.AllFieldZeroWords.statistic line 20
  4. def OAI.MatrixMultiplication.AllFieldZeroWords.complement line 24
  5. theorem OAI.MatrixMultiplication.AllFieldZeroWords.statistic_complement line 28
  6. def OAI.MatrixMultiplication.AllFieldZeroWords.words line 34
  7. theorem OAI.MatrixMultiplication.AllFieldZeroWords.words_injective line 44
  8. theorem OAI.MatrixMultiplication.AllFieldZeroWords.repeat_ratio line 74
  9. theorem OAI.MatrixMultiplication.AllFieldZeroWords.selected_window line 82
  10. theorem OAI.MatrixMultiplication.AllFieldZeroWords.complementary_window line 115