OAI/Computability/QuantumFactoring/SignedSyntaxEmission.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.NetworkEmission.intExprView line 15
  2. def OAI.ExactQuantumFactoring.NetworkEmission.intExprCode line 16
  3. def OAI.ExactQuantumFactoring.NetworkEmission.ratExprView line 17
  4. def OAI.ExactQuantumFactoring.NetworkEmission.ratExprCode line 18
  5. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.intToNatP line 20
  6. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.intExprViewP line 23
  7. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.intExprPosP line 25
  8. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.intExprNegP line 27
  9. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.intExprMkP line 29
  10. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.ratExprViewP line 32
  11. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.ratExprNumP line 34
  12. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.ratExprDenP line 36
  13. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.ratExprMkP line 38
  14. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.ipos line 44
  15. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.ineg line 46
  16. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.imk line 48
  17. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.rnum line 52
  18. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.rden line 54
  19. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.rmk line 56