OAI/Computability/QuantumFactoring/ConcreteExpressionResources.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.PolyExpr.comp_X line 13
2. lemma OAI.ExactQuantumFactoring.PolyExpr.comp_comp line 20
3. def OAI.ExactQuantumFactoring.PolySchemaPoly line 31

   Source documentation

   Substitution-stable, fixed-depth polynomial schemas. In particular this controls the literal syntax of every fixed coefficient, not just its denotation.

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

   Mentions: OAI.ExactQuantumFactoring.PolyExpr