OAI/Analysis/Quantum/PPTSquare/QuadraticBasis.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.QuadraticBasis.powers line 15
2. def OAI.QuadraticBasis.exponent line 18
3. lemma OAI.QuadraticBasis.exponent_apply line 19
4. lemma OAI.QuadraticBasis.exponent_inj line 20
5. lemma OAI.QuadraticBasis.degree_two line 26
6. lemma OAI.QuadraticBasis.exponents_exhaust line 32
7. lemma OAI.QuadraticBasis.homogeneous_expansion line 162
8. lemma OAI.QuadraticBasis.coefficients_nonzero line 181
9. lemma OAI.QuadraticBasis.eval_expansion line 192