OAI/Computability/QuantumFactoring/PolynomialExpressions.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.RatExpr.sum line 13
  2. lemma OAI.ExactQuantumFactoring.RatExpr.eval_sum line 16
  3. inductive OAI.ExactQuantumFactoring.PolyExpr line 24

    Source documentation

    Bounded polynomial arithmetic is itself finite rational syntax.

    inductive PolyExpr (v : Type*) where
…
  4. def OAI.ExactQuantumFactoring.PolyExpr.eval line 34
  5. def OAI.ExactQuantumFactoring.PolyExpr.coeff line 41
  6. lemma OAI.ExactQuantumFactoring.PolyExpr.coeff_correct line 48
  7. def OAI.ExactQuantumFactoring.PolyExpr.sub line 62
  8. def OAI.ExactQuantumFactoring.PolyExpr.const line 63
  9. def OAI.ExactQuantumFactoring.PolyExpr.pow line 64
  10. def OAI.ExactQuantumFactoring.PolyExpr.comp line 68
  11. lemma OAI.ExactQuantumFactoring.PolyExpr.eval_const line 75
  12. lemma OAI.ExactQuantumFactoring.PolyExpr.eval_sub line 77
  13. lemma OAI.ExactQuantumFactoring.PolyExpr.eval_pow line 79
  14. lemma OAI.ExactQuantumFactoring.PolyExpr.eval_comp line 83