OAI/LinearAlgebra/MatrixMultiplication/Completion/GeometricValues.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Readable tensor completion and its finite arithmetic realization.

  1. abbrev OAI.MatrixMultiplication.CompletionGeometricValues.size line 23
  2. theorem OAI.MatrixMultiplication.CompletionGeometricValues.actualPool_decode line 25
  3. theorem OAI.MatrixMultiplication.CompletionGeometricValues.decode_eq_iff_eligible line 31
  4. theorem OAI.MatrixMultiplication.CompletionGeometricValues.raw_XY_normal line 41
  5. theorem OAI.MatrixMultiplication.CompletionGeometricValues.raw_XZ_normal line 71
  6. theorem OAI.MatrixMultiplication.CompletionGeometricValues.raw_YZ_normal line 108