OAI/Computability/QuantumFactoring/HornerEncoding.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.BitArithmetic.horner_sum line 18
2. lemma OAI.ExactQuantumFactoring.BitArithmetic.horner_full line 35
3. lemma OAI.ExactQuantumFactoring.Triangular.outputNumber_value line 42
4. def OAI.ExactQuantumFactoring.reverseBits line 46

   Source documentation

   The physical input word reversal is an explicit wire permutation.

   def reverseBits (b : ℕ) : Equiv.Perm (Basis b) where
   …

   Mentions: OAI.ExactQuantumFactoring.Basis

5. lemma OAI.ExactQuantumFactoring.Triangular.inputNumber_reverse line 52
6. lemma OAI.ExactQuantumFactoring.Triangular.inputNumber_lt line 64
7. lemma OAI.ExactQuantumFactoring.Triangular.inputNumber_bijective line 68