OAI/Computability/QuantumFactoring/ActualDivisorPolynomial.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.FixedSplit.actualBaseNet_poly line 15
2. lemma OAI.ExactQuantumFactoring.FixedSplit.modulusNet_poly line 18
3. lemma OAI.ExactQuantumFactoring.FixedSplit.actualOrderRawNet_poly line 20
4. lemma OAI.ExactQuantumFactoring.FixedSplit.actualOrderNet_poly line 22
5. lemma OAI.ExactQuantumFactoring.FixedSplit.liftedModulus_poly line 24
6. lemma OAI.ExactQuantumFactoring.FixedSplit.roots_poly line 26
7. lemma OAI.ExactQuantumFactoring.FixedSplit.ordersBits_poly line 28
8. lemma OAI.ExactQuantumFactoring.FixedSplit.divisorNet_poly line 44