OAI/Computability/QuantumFactoring/TrialGuessLaw.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ExactQuantumFactoring.OrderTrial.Guesses line 16
2. def OAI.ExactQuantumFactoring.OrderTrial.guessState line 18
3. def OAI.ExactQuantumFactoring.OrderTrial.Retains line 22
4. def OAI.ExactQuantumFactoring.OrderTrial.firstPass line 25
5. def OAI.ExactQuantumFactoring.OrderTrial.secondPass line 27
6. def OAI.ExactQuantumFactoring.OrderTrial.thirdPass line 31
7. lemma OAI.ExactQuantumFactoring.OrderTrial.guess_normalized line 35
8. lemma OAI.ExactQuantumFactoring.OrderTrial.firstPass_mass line 45
9. lemma OAI.ExactQuantumFactoring.OrderTrial.secondPass_mass line 57
10. lemma OAI.ExactQuantumFactoring.OrderTrial.thirdPass_mass line 85