OAI/Computability/QuantumFactoring/ExpressionAt.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ExactQuantumFactoring.NatExprAtline 15 - lemma
OAI.ExactQuantumFactoring.NatExprAt.ofPolyline 19 - lemma
OAI.ExactQuantumFactoring.NatExprAt.pullline 21 - lemma
OAI.ExactQuantumFactoring.NatExprAt.sharedCostline 23 - lemma
OAI.ExactQuantumFactoring.NatExprAt.templateWidthline 25 - lemma
OAI.ExactQuantumFactoring.NatExprAt.operationBoundline 29 - lemma
OAI.ExactQuantumFactoring.NatExprAt.templateline 33 - lemma
OAI.ExactQuantumFactoring.NatExprAt.isOneline 42