OAI/Computability/QuantumFactoring/ExpressionPowerEmission.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.NetworkEmission.exprCode_length line 16
2. lemma OAI.ExactQuantumFactoring.NetworkEmission.exprCode_const line 19
3. lemma OAI.ExactQuantumFactoring.NetworkEmission.exprCode_mul_le line 24
4. def OAI.ExactQuantumFactoring.NetworkEmission.exprPowerStep line 40
5. lemma OAI.ExactQuantumFactoring.NetworkEmission.exprPowerStep_fst line 41
6. lemma OAI.ExactQuantumFactoring.NetworkEmission.exprPowerStep_bound line 45
7. lemma OAI.ExactQuantumFactoring.NetworkEmission.exprPowerStep_start line 56
8. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.exprPowerP line 62
9. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.npow line 84
10. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.iSignedPower line 87
11. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.rSignedPower line 92
12. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.repeatedSuccess line 95