OAI/Computability/QuantumFactoring/FilterExpressionSyntax.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.ExactQuantumFactoring.RatExpr.(instance at line 13) line 13
  2. instance OAI.ExactQuantumFactoring.RatExpr.(instance at line 14) line 14
  3. instance OAI.ExactQuantumFactoring.RatExpr.(instance at line 15) line 15
  4. instance OAI.ExactQuantumFactoring.RatExpr.(instance at line 16) line 16
  5. instance OAI.ExactQuantumFactoring.RatExpr.(instance at line 17) line 17
  6. instance OAI.ExactQuantumFactoring.RatExpr.(instance at line 18) line 18
  7. instance OAI.ExactQuantumFactoring.RatExpr.(instance at line 19) line 19
  8. instance OAI.ExactQuantumFactoring.RatExpr.(instance at line 20) line 20
  9. lemma OAI.ExactQuantumFactoring.RatExpr.eval_num line 21
  10. lemma OAI.ExactQuantumFactoring.RatExpr.eval_plus line 22
  11. lemma OAI.ExactQuantumFactoring.RatExpr.eval_times line 23
  12. lemma OAI.ExactQuantumFactoring.RatExpr.eval_minus line 24
  13. lemma OAI.ExactQuantumFactoring.RatExpr.eval_over line 25
  14. lemma OAI.ExactQuantumFactoring.RatExpr.eval_neg line 26
  15. lemma OAI.ExactQuantumFactoring.RatExpr.eval_inv line 27
  16. lemma OAI.ExactQuantumFactoring.RatExpr.eval_power line 28
  17. instance OAI.ExactQuantumFactoring.PolyExpr.(instance at line 32) line 32
  18. instance OAI.ExactQuantumFactoring.PolyExpr.(instance at line 33) line 33
  19. instance OAI.ExactQuantumFactoring.PolyExpr.(instance at line 34) line 34
  20. instance OAI.ExactQuantumFactoring.PolyExpr.(instance at line 35) line 35
  21. instance OAI.ExactQuantumFactoring.PolyExpr.(instance at line 36) line 36
  22. instance OAI.ExactQuantumFactoring.PolyExpr.(instance at line 37) line 37
  23. lemma OAI.ExactQuantumFactoring.PolyExpr.eval_num line 38
  24. lemma OAI.ExactQuantumFactoring.PolyExpr.eval_plus line 39
  25. lemma OAI.ExactQuantumFactoring.PolyExpr.eval_times line 40
  26. lemma OAI.ExactQuantumFactoring.PolyExpr.eval_minus line 41
  27. lemma OAI.ExactQuantumFactoring.PolyExpr.eval_neg line 42
  28. lemma OAI.ExactQuantumFactoring.PolyExpr.eval_power line 43