OAI/LinearAlgebra/MatrixMultiplication/Arithmetic/ProgramComposition.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Division-free arithmetic programs over a field and their operation counts.

  1. def OAI.MatrixMultiplication.Arithmetic.Gate.mapInput line 17
  2. theorem OAI.MatrixMultiplication.Arithmetic.Gate.eval_mapInput line 24
  3. theorem OAI.MatrixMultiplication.Arithmetic.Gate.cost_mapInput line 30
  4. def OAI.MatrixMultiplication.Arithmetic.Gate.mapSource line 34
  5. theorem OAI.MatrixMultiplication.Arithmetic.Gate.eval_mapSource line 43
  6. theorem OAI.MatrixMultiplication.Arithmetic.Gate.cost_mapSource line 55
  7. def OAI.MatrixMultiplication.Arithmetic.Program.mapInput line 70
  8. theorem OAI.MatrixMultiplication.Arithmetic.Program.eval_mapInput line 74
  9. theorem OAI.MatrixMultiplication.Arithmetic.Program.cost_mapInput line 87
  10. def OAI.MatrixMultiplication.Arithmetic.Program.mapSource line 93
  11. theorem OAI.MatrixMultiplication.Arithmetic.Program.eval_mapSource line 97
  12. theorem OAI.MatrixMultiplication.Arithmetic.Program.cost_mapSource line 111
  13. structure OAI.MatrixMultiplication.Arithmetic.Program.Substituted line 117
  14. def OAI.MatrixMultiplication.Arithmetic.Program.Substituted.step line 130
  15. def OAI.MatrixMultiplication.Arithmetic.Program.substitute line 154