OAI/LinearAlgebra/MatrixMultiplication/FieldConstruction/FinalState.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Tensor extraction over arbitrary fields and its asymptotic rate.

  1. abbrev OAI.MatrixMultiplication.AllFieldFinalState.InitialIndex line 18
  2. abbrev OAI.MatrixMultiplication.AllFieldFinalState.CIndex line 19
  3. abbrev OAI.MatrixMultiplication.AllFieldFinalState.Index line 20
  4. def OAI.MatrixMultiplication.AllFieldFinalState.history line 22
  5. theorem OAI.MatrixMultiplication.AllFieldFinalState.history_terminal line 27
  6. theorem OAI.MatrixMultiplication.AllFieldFinalState.terminal_resident_final line 35
  7. def OAI.MatrixMultiplication.AllFieldFinalState.toState line 54
  8. def OAI.MatrixMultiplication.AllFieldFinalState.fromState line 57
  9. def OAI.MatrixMultiplication.AllFieldFinalState.indexEquiv line 67
  10. abbrev OAI.MatrixMultiplication.AllFieldFinalState.Words line 87
  11. abbrev OAI.MatrixMultiplication.AllFieldFinalState.InitialWords line 88
  12. abbrev OAI.MatrixMultiplication.AllFieldFinalState.ZeroWords line 90
  13. abbrev OAI.MatrixMultiplication.AllFieldFinalState.CWords line 92
  14. abbrev OAI.MatrixMultiplication.AllFieldFinalState.Parts line 93
  15. instance OAI.MatrixMultiplication.AllFieldFinalState.wordsFintype line 96
  16. def OAI.MatrixMultiplication.AllFieldFinalState.grouped line 99
  17. def OAI.MatrixMultiplication.AllFieldFinalState.stateWord line 105
  18. theorem OAI.MatrixMultiplication.AllFieldFinalState.grouped_coefficient line 110
  19. def OAI.MatrixMultiplication.AllFieldFinalState.groupedMap line 127
  20. def OAI.MatrixMultiplication.AllFieldFinalState.initialTensor line 137
  21. def OAI.MatrixMultiplication.AllFieldFinalState.zeroTensor line 143
  22. def OAI.MatrixMultiplication.AllFieldFinalState.cTensor line 149
  23. def OAI.MatrixMultiplication.AllFieldFinalState.partsTensor line 155
  24. def OAI.MatrixMultiplication.AllFieldFinalState.joinParts line 162
  25. theorem OAI.MatrixMultiplication.AllFieldFinalState.parts_coefficient line 167
  26. def OAI.MatrixMultiplication.AllFieldFinalState.partsMap line 176
  27. def OAI.MatrixMultiplication.AllFieldFinalState.map line 186