OAI/LinearAlgebra/MatrixMultiplication/Completion/HierarchyWords.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Readable tensor completion and its finite arithmetic realization.

  1. structure OAI.MatrixMultiplication.CompletionHierarchyWords.ReadableHierarchy line 17
  2. def OAI.MatrixMultiplication.CompletionHierarchyWords.longX line 52
  3. def OAI.MatrixMultiplication.CompletionHierarchyWords.longY line 53
  4. def OAI.MatrixMultiplication.CompletionHierarchyWords.longZ line 54
  5. theorem OAI.MatrixMultiplication.CompletionHierarchyWords.longCoordinates_injective line 57
  6. def OAI.MatrixMultiplication.CompletionHierarchyWords.Represents line 68
  7. def OAI.MatrixMultiplication.CompletionHierarchyWords.eligible line 74
  8. def OAI.MatrixMultiplication.CompletionHierarchyWords.readXYX line 78
  9. theorem OAI.MatrixMultiplication.CompletionHierarchyWords.readXYX_on_original_word line 82
  10. def OAI.MatrixMultiplication.CompletionHierarchyWords.readXYY line 93
  11. theorem OAI.MatrixMultiplication.CompletionHierarchyWords.readXYY_on_original_word line 97
  12. def OAI.MatrixMultiplication.CompletionHierarchyWords.readXZX line 108
  13. theorem OAI.MatrixMultiplication.CompletionHierarchyWords.readXZX_on_original_word line 112
  14. def OAI.MatrixMultiplication.CompletionHierarchyWords.readXZZ line 123
  15. theorem OAI.MatrixMultiplication.CompletionHierarchyWords.readXZZ_on_original_word line 127
  16. def OAI.MatrixMultiplication.CompletionHierarchyWords.readYZY line 138
  17. theorem OAI.MatrixMultiplication.CompletionHierarchyWords.readYZY_on_original_word line 142
  18. def OAI.MatrixMultiplication.CompletionHierarchyWords.readYZZ line 153
  19. theorem OAI.MatrixMultiplication.CompletionHierarchyWords.readYZZ_on_original_word line 157
  20. theorem OAI.MatrixMultiplication.CompletionHierarchyWords.readable_XY line 168
  21. theorem OAI.MatrixMultiplication.CompletionHierarchyWords.readable_XZ line 180
  22. theorem OAI.MatrixMultiplication.CompletionHierarchyWords.readable_YZ line 192
  23. theorem OAI.MatrixMultiplication.CompletionHierarchyWords.represented_word_unique line 204
  24. theorem OAI.MatrixMultiplication.CompletionHierarchyWords.eligible_appendCode_iff line 214
  25. theorem OAI.MatrixMultiplication.CompletionHierarchyWords.represented_fine_eq line 242
  26. theorem OAI.MatrixMultiplication.CompletionHierarchyWords.eligible_appendCode_iff_of_represents line 250
  27. theorem OAI.MatrixMultiplication.CompletionHierarchyWords.root_eligible_iff line 264
  28. def OAI.MatrixMultiplication.CompletionHierarchyWords.terminalWord line 287
  29. theorem OAI.MatrixMultiplication.CompletionHierarchyWords.terminalWord_record line 299
  30. theorem OAI.MatrixMultiplication.CompletionHierarchyWords.terminalWord_of_represents line 305
  31. theorem OAI.MatrixMultiplication.CompletionHierarchyWords.terminal_eligible_iff line 314