OAI/Computability/QuantumFactoring/CanonicalResidueCircuit.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.BitArithmetic.dividesOn line 19
  2. lemma OAI.ExactQuantumFactoring.BitArithmetic.dividesOn_value line 21
  3. lemma OAI.ExactQuantumFactoring.BitArithmetic.dividesOn_count line 24
  4. def OAI.ExactQuantumFactoring.BitArithmetic.leastDivisorTest line 31
  5. lemma OAI.ExactQuantumFactoring.BitArithmetic.leastDivisorTest_value line 34
  6. lemma OAI.ExactQuantumFactoring.BitArithmetic.leastDivisorTest_count line 43
  7. def OAI.ExactQuantumFactoring.BitArithmetic.componentCongruence line 60
  8. lemma OAI.ExactQuantumFactoring.BitArithmetic.componentCongruence_value line 66
  9. def OAI.ExactQuantumFactoring.BitArithmetic.tableCanonicalNet line 87
  10. lemma OAI.ExactQuantumFactoring.BitArithmetic.tableCanonicalNet_value line 91
  11. def OAI.ExactQuantumFactoring.BitArithmetic.componentCongruenceBound line 110
  12. lemma OAI.ExactQuantumFactoring.BitArithmetic.componentCongruence_count line 114
  13. def OAI.ExactQuantumFactoring.BitArithmetic.tableCanonicalBound line 130
  14. lemma OAI.ExactQuantumFactoring.BitArithmetic.tableCanonicalNet_count line 133