OAI/Computability/QuantumFactoring/PolynomialExpressionResources.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.RatExprPoly.ite line 13
2. lemma OAI.ExactQuantumFactoring.RatExprPoly.sum line 19
3. def OAI.ExactQuantumFactoring.PolyExprPoly line 27

   Source documentation

   Every fixed-index coefficient of this family has polynomial syntax.

   def PolyExprPoly {v : ℕ → Type*} (a : ∀ n, PolyExpr (v n)) : Prop :=
   …

   Mentions: OAI.ExactQuantumFactoring.PolyExpr

4. lemma OAI.ExactQuantumFactoring.PolyExprPoly.C line 31
5. lemma OAI.ExactQuantumFactoring.PolyExprPoly.X line 36
6. lemma OAI.ExactQuantumFactoring.PolyExprPoly.constant line 41
7. lemma OAI.ExactQuantumFactoring.PolyExprPoly.add line 43
8. lemma OAI.ExactQuantumFactoring.PolyExprPoly.negation line 45
9. lemma OAI.ExactQuantumFactoring.PolyExprPoly.sub line 47
10. lemma OAI.ExactQuantumFactoring.PolyExprPoly.mul line 49
11. lemma OAI.ExactQuantumFactoring.PolyExprPoly.pow line 51
12. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.coveringPow_maxConst line 59
13. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.coveringPow_weight line 67
14. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.coveringPow_poly line 74