OAI/Computability/QuantumFactoring/StaticPredicates.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.BitArithmetic.equalOn line 15
2. lemma OAI.ExactQuantumFactoring.BitArithmetic.equalOn_value line 18
3. lemma OAI.ExactQuantumFactoring.BitArithmetic.equalOn_count line 23
4. def OAI.ExactQuantumFactoring.BitArithmetic.constMod line 29
5. lemma OAI.ExactQuantumFactoring.BitArithmetic.constMod_value line 32
6. lemma OAI.ExactQuantumFactoring.BitArithmetic.constMod_count line 37
7. def OAI.ExactQuantumFactoring.BitArithmetic.dividesNet line 42
8. lemma OAI.ExactQuantumFactoring.BitArithmetic.dividesNet_value line 45
9. lemma OAI.ExactQuantumFactoring.BitArithmetic.dividesNet_count line 51
10. def OAI.ExactQuantumFactoring.BitArithmetic.constPowMod line 59

    Source documentation

    Static modulus and exponent; exponent wiring is reversed explicitly.

    def constPowMod (w s j : ℕ) : BooleanNetwork w w :=
    …

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

11. lemma OAI.ExactQuantumFactoring.BitArithmetic.constPowMod_value line 63
12. lemma OAI.ExactQuantumFactoring.BitArithmetic.constPowMod_count line 81
13. def OAI.ExactQuantumFactoring.BitArithmetic.powerOneNet line 87
14. lemma OAI.ExactQuantumFactoring.BitArithmetic.powerOneNet_value line 90
15. lemma OAI.ExactQuantumFactoring.BitArithmetic.powerOneNet_count line 96