OAI/Computability/QuantumFactoring/CompletionFilterPolynomial.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.RatExprPoly.ofHeight line 16
2. lemma OAI.ExactQuantumFactoring.Completion.Expressions.ordinaryMass_poly line 21
3. lemma OAI.ExactQuantumFactoring.Completion.Expressions.coefficient_poly line 25
4. lemma OAI.ExactQuantumFactoring.Completion.Expressions.guess_poly line 31
5. lemma OAI.ExactQuantumFactoring.Completion.Expressions.listRateCoin_poly line 37
6. lemma OAI.ExactQuantumFactoring.Completion.Expressions.orderRateCoin_poly line 41
7. lemma OAI.ExactQuantumFactoring.retentionNet_at line 46
8. lemma OAI.ExactQuantumFactoring.Completion.predicateFilter_at line 54