OAI/Computability/QuantumFactoring/RowNetwork.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.Triangular.rowIndex line 16
2. lemma OAI.ExactQuantumFactoring.Triangular.rowIndex_val line 19
3. def OAI.ExactQuantumFactoring.Triangular.rowNetwork line 27

   Source documentation

   Combining one triangular row is just a bit permutation and masked ANDs; no arbitrary phase or exponentially large truth table is present.

   def rowNetwork {b : ℕ} (j : Fin b) : BooleanNetwork b b :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

4. lemma OAI.ExactQuantumFactoring.Triangular.rowNetwork_count line 32
5. lemma OAI.ExactQuantumFactoring.Triangular.rowNetwork_bit line 43
6. lemma OAI.ExactQuantumFactoring.Triangular.rowNetwork_number line 49