OAI/Computability/QuantumFactoring/RawTrialFields.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.OrderTrial.rawMode line 17
  2. def OAI.ExactQuantumFactoring.OrderTrial.rawSample line 19
  3. def OAI.ExactQuantumFactoring.OrderTrial.rawGuesses line 23
  4. def OAI.ExactQuantumFactoring.OrderTrial.rawDen line 26
  5. def OAI.ExactQuantumFactoring.OrderTrial.rawNum line 28
  6. def OAI.ExactQuantumFactoring.OrderTrial.rawResidue line 30
  7. def OAI.ExactQuantumFactoring.OrderTrial.rawCoin line 33
  8. lemma OAI.ExactQuantumFactoring.OrderTrial.rawMode_eval line 37
  9. lemma OAI.ExactQuantumFactoring.OrderTrial.rawSample_eval line 40
  10. lemma OAI.ExactQuantumFactoring.OrderTrial.rawGuesses_eval line 43
  11. lemma OAI.ExactQuantumFactoring.OrderTrial.rawDen_eval line 46
  12. lemma OAI.ExactQuantumFactoring.OrderTrial.rawNum_eval line 50
  13. lemma OAI.ExactQuantumFactoring.OrderTrial.rawResidue_eval line 54
  14. lemma OAI.ExactQuantumFactoring.OrderTrial.rawCoin_eval line 58
  15. def OAI.ExactQuantumFactoring.OrderTrial.toWidth line 63
  16. lemma OAI.ExactQuantumFactoring.OrderTrial.toWidth_value line 65
  17. lemma OAI.ExactQuantumFactoring.OrderTrial.toWidth_count line 68