OAI/Computability/QuantumFactoring/AppendRegister.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ExactQuantumFactoring.rightRegisterline 13 - lemma
OAI.ExactQuantumFactoring.append_rightRegisterline 15 - lemma
OAI.ExactQuantumFactoring.append_right_injectiveline 20 - lemma
OAI.ExactQuantumFactoring.append_replace_rightline 26 - def
OAI.ExactQuantumFactoring.rightProgramline 41 - lemma
OAI.ExactQuantumFactoring.rightProgram_basisline 44 - lemma
OAI.ExactQuantumFactoring.rightProgram_entryline 52