OAI/Computability/QuantumFactoring/RationalConditionals.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.IntExpr.ifLe line 14
  2. lemma OAI.ExactQuantumFactoring.IntExpr.eval_ifLe line 16
  3. def OAI.ExactQuantumFactoring.RatExpr.ifNatLe line 28
  4. lemma OAI.ExactQuantumFactoring.RatExpr.eval_ifNatLe line 30
  5. def OAI.ExactQuantumFactoring.RatExpr.ifIntLe line 36
  6. lemma OAI.ExactQuantumFactoring.RatExpr.eval_ifIntLe line 38
  7. def OAI.ExactQuantumFactoring.RatExpr.ifLe line 47
  8. lemma OAI.ExactQuantumFactoring.RatExpr.eval_ifLe line 51
  9. def OAI.ExactQuantumFactoring.RatExpr.ifLt line 63
  10. def OAI.ExactQuantumFactoring.RatExpr.ifEq line 64
  11. def OAI.ExactQuantumFactoring.RatExpr.max line 65
  12. def OAI.ExactQuantumFactoring.RatExpr.min line 66
  13. lemma OAI.ExactQuantumFactoring.RatExpr.eval_ifLt line 67
  14. lemma OAI.ExactQuantumFactoring.RatExpr.eval_ifEq line 73
  15. lemma OAI.ExactQuantumFactoring.RatExpr.eval_max line 82
  16. lemma OAI.ExactQuantumFactoring.RatExpr.eval_min line 84