OAI/Computability/QuantumFactoring/NativeAIGMul.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.NativeAIG.isZero line 14
2. lemma OAI.ExactQuantumFactoring.NativeAIG.isZero_eq line 15
3. def OAI.ExactQuantumFactoring.NativeAIG.mulLoop line 20
4. def OAI.ExactQuantumFactoring.NativeAIG.mulBlast line 27
5. def OAI.ExactQuantumFactoring.NativeAIG.mul line 31
6. lemma OAI.ExactQuantumFactoring.NativeAIG.mulLoop_rel line 34
7. lemma OAI.ExactQuantumFactoring.NativeAIG.mulBlast_rel line 69
8. lemma OAI.ExactQuantumFactoring.NativeAIG.mul_rel line 96