OAI/LinearAlgebra/MatrixMultiplication/Tensor/ComplexElementary.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Finite coefficient tensors and their algebraic transformations.

  1. inductive OAI.MatrixMultiplication.Foundation.Elementary.BoundaryTerm line 9
  2. def OAI.MatrixMultiplication.Foundation.Elementary.BoundaryTerm.x line 15
  3. def OAI.MatrixMultiplication.Foundation.Elementary.BoundaryTerm.y line 20
  4. def OAI.MatrixMultiplication.Foundation.Elementary.BoundaryTerm.z line 25
  5. def OAI.MatrixMultiplication.Foundation.Elementary.BoundaryTerm.all line 30
  6. def OAI.MatrixMultiplication.Foundation.Elementary.testA line 34
  7. def OAI.MatrixMultiplication.Foundation.Elementary.testB line 35
  8. def OAI.MatrixMultiplication.Foundation.Elementary.testC line 36
  9. theorem OAI.MatrixMultiplication.Foundation.Elementary.local_tests_exhaust line 38
  10. def OAI.MatrixMultiplication.Foundation.Elementary.localDegree line 46
  11. theorem OAI.MatrixMultiplication.Foundation.Elementary.localDegree_eq line 49
  12. def OAI.MatrixMultiplication.Foundation.Elementary.retained line 55
  13. def OAI.MatrixMultiplication.Foundation.Elementary.triples line 58
  14. theorem OAI.MatrixMultiplication.Foundation.Elementary.retained_triples_count line 63
  15. theorem OAI.MatrixMultiplication.Foundation.Elementary.retained_b_triples_count line 65
  16. theorem OAI.MatrixMultiplication.Foundation.Elementary.retained_c_triples_count line 68