OAI/LinearAlgebra/MatrixMultiplication/Completion/ProgramPrefixes.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Readable tensor completion and its finite arithmetic realization.

  1. theorem OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.labelRecordOf_eq_iff line 15
  2. theorem OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.append_record_eq_iff line 37
  3. theorem OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.recode_record_eq_iff line 67
  4. theorem OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.pow_record_eq_iff line 81
  5. theorem OAI.MatrixMultiplication.CompletionLabels.completionLocalProgram_label_root line 144
  6. theorem OAI.MatrixMultiplication.CompletionLabels.completionLocalProgram_pair_root line 158
  7. theorem OAI.MatrixMultiplication.CompletionLabels.completionLocalProgram_label_slot line 169
  8. theorem OAI.MatrixMultiplication.CompletionLabels.completionLocalProgram_pair_slot line 188
  9. theorem OAI.MatrixMultiplication.CompletionLabels.patternProgram_record_eq_iff line 202
  10. theorem OAI.MatrixMultiplication.CompletionLabels.completionProgram_record_eq_iff line 233