OAI/Computability/QuantumFactoring/ReadOnlyCircuit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.Gate.arity_pos line 17
2. def OAI.ExactQuantumFactoring.Instruction.target line 21
3. lemma OAI.ExactQuantumFactoring.Primitive.nonTarget_zero line 24
4. lemma OAI.ExactQuantumFactoring.Gate.base_nonTarget_zero line 45
5. lemma OAI.ExactQuantumFactoring.Gate.nonTarget_zero line 56

   Source documentation

   In the literal fixed alphabet, all but the final wire are controls. The inverse and added-control variants preserve these same wires.

   lemma Gate.nonTarget_zero (g : Gate) (x y : Basis g.arity) (i : Fin g.arity)
       (hi : i.val+1<g.arity) (hne : x i≠y i) : g.localMatrix x y=0 := by
   …

   Mentions: OAI.ExactQuantumFactoring.Gate, OAI.ExactQuantumFactoring.Basis

6. lemma OAI.ExactQuantumFactoring.Instruction.nonzero_eq line 84