OAI/Computability/QuantumFactoring/BitStackPowers.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.ExactQuantumFactoring.BitStackProgram.bits_length_powline 11 - def
OAI.ExactQuantumFactoring.BitStackProgram.powerStepline 18 - lemma
OAI.ExactQuantumFactoring.BitStackProgram.powerStep_iterateline 19 - def
OAI.ExactQuantumFactoring.BitStackProgram.Procedure.binaryPowline 24 - lemma
OAI.ExactQuantumFactoring.BitStackProgram.Emits.natPowline 45 - lemma
OAI.ExactQuantumFactoring.BitStackProgram.Emits.natEvenline 47