OAI/LinearAlgebra/MatrixMultiplication/Completion/Scripts.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Readable tensor completion and its finite arithmetic realization.

  1. inductive OAI.MatrixMultiplication.RecursiveCompletion.Script line 13
  2. def OAI.MatrixMultiplication.RecursiveCompletion.Script.factors line 19
  3. def OAI.MatrixMultiplication.RecursiveCompletion.Script.Coord line 23
  4. instance OAI.MatrixMultiplication.RecursiveCompletion.Script.coordFintype line 27
  5. def OAI.MatrixMultiplication.RecursiveCompletion.Script.tensor line 34
  6. def OAI.MatrixMultiplication.RecursiveCompletion.Script.order line 39
  7. def OAI.MatrixMultiplication.RecursiveCompletion.Script.degree line 43
  8. def OAI.MatrixMultiplication.RecursiveCompletion.Script.approximation line 47
  9. theorem OAI.MatrixMultiplication.RecursiveCompletion.Script.rank_power line 58
  10. def OAI.MatrixMultiplication.RecursiveCompletion.Script.dual line 65
  11. def OAI.MatrixMultiplication.RecursiveCompletion.Script.curve line 68
  12. def OAI.MatrixMultiplication.RecursiveCompletion.Script.square line 70
  13. theorem OAI.MatrixMultiplication.RecursiveCompletion.Script.dual_factors line 73
  14. theorem OAI.MatrixMultiplication.RecursiveCompletion.Script.curve_factors line 74
  15. theorem OAI.MatrixMultiplication.RecursiveCompletion.Script.square_factors line 75