OAI/Computability/QuantumFactoring/SplitDecoderPolynomial.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.BitArithmetic.firstProperNet_count line 15
2. lemma OAI.ExactQuantumFactoring.NetworkAt.addNet line 29
3. lemma OAI.ExactQuantumFactoring.NetworkAt.subNet line 31
4. lemma OAI.ExactQuantumFactoring.NetworkAt.divNet line 33
5. lemma OAI.ExactQuantumFactoring.NetworkAt.modNet line 36
6. lemma OAI.ExactQuantumFactoring.NetworkAt.properOn line 39
7. lemma OAI.ExactQuantumFactoring.NetworkAt.evenOn line 45
8. lemma OAI.ExactQuantumFactoring.NetworkAt.halfWord line 48
9. lemma OAI.ExactQuantumFactoring.NetworkAt.halfPowerBits line 51
10. lemma OAI.ExactQuantumFactoring.NetworkAt.shiftedHalfBits line 56
11. lemma OAI.ExactQuantumFactoring.NetworkAt.candidateBits line 62
12. lemma OAI.ExactQuantumFactoring.NetworkAt.firstProperNet line 68
13. lemma OAI.ExactQuantumFactoring.NetworkAt.rootOn line 78
14. lemma OAI.ExactQuantumFactoring.NetworkAt.rootsOn line 84