OAI/Computability/QuantumFactoring/ExpressionAt.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.NatExprAt line 15
  2. lemma OAI.ExactQuantumFactoring.NatExprAt.ofPoly line 19
  3. lemma OAI.ExactQuantumFactoring.NatExprAt.pull line 21
  4. lemma OAI.ExactQuantumFactoring.NatExprAt.sharedCost line 23
  5. lemma OAI.ExactQuantumFactoring.NatExprAt.templateWidth line 25
  6. lemma OAI.ExactQuantumFactoring.NatExprAt.operationBound line 29
  7. lemma OAI.ExactQuantumFactoring.NatExprAt.template line 33
  8. lemma OAI.ExactQuantumFactoring.NatExprAt.isOne line 42