OAI/LinearAlgebra/MatrixMultiplication/Completion/Termination.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Readable tensor completion and its finite arithmetic realization.

  1. def OAI.MatrixMultiplication.CompletionTermination.tensor line 18
  2. theorem OAI.MatrixMultiplication.CompletionTermination.support_iff line 22
  3. def OAI.MatrixMultiplication.CompletionTermination.leftMap line 28
  4. def OAI.MatrixMultiplication.CompletionTermination.middleMap line 31
  5. def OAI.MatrixMultiplication.CompletionTermination.rightMap line 34
  6. theorem OAI.MatrixMultiplication.CompletionTermination.restriction line 39
  7. def OAI.MatrixMultiplication.CompletionTermination.approximation line 46
  8. def OAI.MatrixMultiplication.CompletionTermination.Leaf line 52
  9. instance OAI.MatrixMultiplication.CompletionTermination.leafFintype line 55
  10. def OAI.MatrixMultiplication.CompletionTermination.leafEquiv line 59
  11. def OAI.MatrixMultiplication.CompletionTermination.retainedLeafEquiv line 71
  12. theorem OAI.MatrixMultiplication.CompletionTermination.retainedLeafEquiv_coordinates line 78