OAI/Computability/QuantumFactoring/TriangularCircuit.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ExactQuantumFactoring.Triangular.work line 19
  2. abbrev OAI.ExactQuantumFactoring.Triangular.width line 20
  3. def OAI.ExactQuantumFactoring.Triangular.encode line 22
  4. lemma OAI.ExactQuantumFactoring.Triangular.encode_injective line 25
  5. def OAI.ExactQuantumFactoring.Triangular.dataWire line 41
  6. lemma OAI.ExactQuantumFactoring.Triangular.encode_bit line 43
  7. lemma OAI.ExactQuantumFactoring.Triangular.encode_update line 49
  8. lemma OAI.ExactQuantumFactoring.Triangular.translation_count_forward line 55
  9. lemma OAI.ExactQuantumFactoring.Triangular.translation_count_backward line 62
  10. def OAI.ExactQuantumFactoring.Triangular.translation line 69
  11. def OAI.ExactQuantumFactoring.Triangular.rowPerm line 74
  12. lemma OAI.ExactQuantumFactoring.Triangular.translate_encode line 80
  13. lemma OAI.ExactQuantumFactoring.Triangular.translation_basis line 88
  14. lemma OAI.ExactQuantumFactoring.Triangular.translation_apply line 96
  15. def OAI.ExactQuantumFactoring.Triangular.rowCircuit line 101
  16. lemma OAI.ExactQuantumFactoring.Triangular.rowCircuit_apply line 104
  17. def OAI.ExactQuantumFactoring.Triangular.triPrefix line 118
  18. lemma OAI.ExactQuantumFactoring.Triangular.triPrefix_apply line 122
  19. lemma OAI.ExactQuantumFactoring.Triangular.rowCircuit_length line 133
  20. lemma OAI.ExactQuantumFactoring.Triangular.triPrefix_length line 145