OAI/Computability/QuantumFactoring/PrimalityEmission.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.splitOn line 16
2. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.constMod line 21
3. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.divides line 24
4. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.constPowMod line 27
5. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.powerOne line 30
6. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.orderTests line 33
7. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.properDivisor line 38
8. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.noSmallDivisor line 41
9. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.allCongruences line 47
10. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.aksBranch line 52
11. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.aksStaticBranch line 57
12. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.primality line 66