OAI/Computability/QuantumFactoring/RationalExpressions.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ExactQuantumFactoring.RatExpr line 14

    Source documentation

    Rational arithmetic as fixed finite syntax over nonnegative registers. No canonical-fraction reduction or unit-cost large-integer operation is required.

    structure RatExpr (v : Type*) where
…
  2. def OAI.ExactQuantumFactoring.RatExpr.eval line 21
  3. def OAI.ExactQuantumFactoring.RatExpr.ofNat line 22
  4. def OAI.ExactQuantumFactoring.RatExpr.ofInt line 23
  5. def OAI.ExactQuantumFactoring.RatExpr.const line 24
  6. def OAI.ExactQuantumFactoring.RatExpr.normalize line 25
  7. def OAI.ExactQuantumFactoring.RatExpr.add line 28
  8. def OAI.ExactQuantumFactoring.RatExpr.negation line 32
  9. def OAI.ExactQuantumFactoring.RatExpr.sub line 33
  10. def OAI.ExactQuantumFactoring.RatExpr.mul line 34
  11. def OAI.ExactQuantumFactoring.RatExpr.inverse line 35
  12. def OAI.ExactQuantumFactoring.RatExpr.div line 37
  13. def OAI.ExactQuantumFactoring.RatExpr.pow line 38
  14. lemma OAI.ExactQuantumFactoring.RatExpr.eval_ofNat line 42
  15. lemma OAI.ExactQuantumFactoring.RatExpr.eval_ofInt line 44
  16. lemma OAI.ExactQuantumFactoring.RatExpr.eval_const line 46
  17. lemma OAI.ExactQuantumFactoring.RatExpr.eval_normalize line 48
  18. lemma OAI.ExactQuantumFactoring.RatExpr.normalize_den_pos line 53
  19. lemma OAI.ExactQuantumFactoring.RatExpr.eval_add line 56
  20. lemma OAI.ExactQuantumFactoring.RatExpr.eval_negation line 63
  21. lemma OAI.ExactQuantumFactoring.RatExpr.eval_sub line 65
  22. lemma OAI.ExactQuantumFactoring.RatExpr.eval_mul line 67
  23. lemma OAI.ExactQuantumFactoring.RatExpr.eval_inverse line 69
  24. lemma OAI.ExactQuantumFactoring.RatExpr.eval_div line 82
  25. lemma OAI.ExactQuantumFactoring.RatExpr.eval_pow line 84