OAI/LinearAlgebra/MatrixFields/Construction/FinalState.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinalState.InitialIndex line 21
  2. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinalState.CIndex line 22
  3. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinalState.Index line 23
  4. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinalState.history line 25
  5. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinalState.history_terminal line 30
  6. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinalState.terminal_resident_final line 38
  7. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinalState.toState line 57
  8. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinalState.fromState line 60
  9. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinalState.indexEquiv line 70
  10. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinalState.Words line 90
  11. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinalState.InitialWords line 91
  12. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinalState.ZeroWords line 93
  13. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinalState.CWords line 95
  14. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinalState.Parts line 96
  15. instance OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinalState.wordsFintype line 99
  16. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinalState.grouped line 102
  17. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinalState.stateWord line 108
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinalState.grouped_coefficient line 113
  19. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinalState.groupedMap line 133
  20. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinalState.initialTensor line 143
  21. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinalState.zeroTensor line 149
  22. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinalState.cTensor line 155
  23. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinalState.partsTensor line 161
  24. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinalState.joinParts line 168
  25. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinalState.parts_coefficient line 173
  26. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinalState.partsMap line 182
  27. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldFinalState.map line 192