OAI/Computability/QuantumFactoring/CircuitPreparationEmission.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.CircuitEmission.hadamardOp line 13
2. lemma OAI.ExactQuantumFactoring.CircuitEmission.erase_hadamardAt line 14
3. lemma OAI.ExactQuantumFactoring.CircuitEmission.erase_hadamardPrefix line 15
4. def OAI.ExactQuantumFactoring.CircuitEmission.Emission.hadamardOpP line 22
5. def OAI.ExactQuantumFactoring.CircuitEmission.Emission.hadamardPrefixP line 25
6. lemma OAI.ExactQuantumFactoring.CircuitEmission.OpsEmits.hadamards line 31
7. lemma OAI.ExactQuantumFactoring.CircuitEmission.OpsEmits.left line 34
8. lemma OAI.ExactQuantumFactoring.CircuitEmission.OpsEmits.right line 38
9. lemma OAI.ExactQuantumFactoring.CircuitEmission.OpsEmits.parallel line 43
10. lemma OAI.ExactQuantumFactoring.CircuitEmission.OpsEmits.target line 47
11. lemma OAI.ExactQuantumFactoring.CircuitEmission.OpsEmits.prepared line 52