OAI/Computability/QuantumFactoring/TwoAdicCircuit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.twoadic_lt_width line 17
2. lemma OAI.ExactQuantumFactoring.twoadic_eq_iff line 22
3. def OAI.ExactQuantumFactoring.BitArithmetic.bequiv line 34
4. lemma OAI.ExactQuantumFactoring.BitArithmetic.bequiv_value line 35
5. lemma OAI.ExactQuantumFactoring.BitArithmetic.bequiv_count line 39
6. def OAI.ExactQuantumFactoring.BitArithmetic.sameTwoVal line 45

   Source documentation

   Equality of exact dyadic valuations by bounded divisibility tests. The parameter is the word width, not an input-dependent search cap.

   def sameTwoVal {k n : ℕ} (a b : BooleanNetwork k n) : BooleanNetwork k 1 :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

7. lemma OAI.ExactQuantumFactoring.BitArithmetic.sameTwoVal_value line 49
8. lemma OAI.ExactQuantumFactoring.BitArithmetic.sameTwoVal_count line 57